(*<*)
theory Trie2 = Main:;
(*>*)

text {* Die obige Definition der Funktion @{term update} hat den Nachteil, dass 
in der Assoziationliste unn\"otige Information enthalten sein kann: 
Wenn man an die Liste ein neues Assoziationspaar zu einem Zeichen anf\"ugt, das 
schon in der Liste enthalten ist, bleibt das urspr\"ungliche Paar in der Liste
enthalten und ist nur nicht mehr durch die Funktion @{term assoc} zug\"anglich.

Diesen Nachteil kann man beheben, indem man eine (noch zu definierende) Funktion *}

consts overwrite :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b) list \<Rightarrow> ('a * 'b) list"

text {* verwendet, die eine Assoziation zu einem Zeichen, das schon in der Liste
vorkommt, durch ein neues Paar ersetzt.

Definieren Sie die Funktion @{term overwrite}, ver\"andern Sie die Funktion 
@{term modify}, so dass sie die Funktion @{term overwrite}
verwendet und zeigen Sie, wieder den Zusammenhang zwischen @{term modify} und 
@{term lookup}.
*}

(*<*)
end;
(*>*)