diff -r 6878bb02a7f9 -r 16481a4cc9f3 doc-src/TutorialI/Trie/document/Trie.tex
--- a/doc-src/TutorialI/Trie/document/Trie.tex	Thu May 10 09:48:50 2001 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Thu May 10 13:44:44 2001 +0200
@@ -123,7 +123,29 @@
 \isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals
 of the induction up in such a way that case distinction on \isa{bs} makes
 sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
-and stable proofs.%
+and stable proofs.
+
+\begin{exercise}
+  Modify \isa{update} (and its type) such that it allows both insertion and
+  deletion of entries with a single function.  Prove (a modified version of)
+  the main theorem above.
+  Optimize you function such that it shrinks tries after
+  deletion, if possible.
+\end{exercise}
+
+\begin{exercise}
+  Write an improved version of \isa{update} that does not suffer from the
+  space leak (pointed out above) caused by not deleting overwritten entries
+  from the association list. Prove the main theorem for your improved
+  \isa{update}.
+\end{exercise}
+
+\begin{exercise}
+  Conceptually, each node contains a mapping from letters to optional
+  subtries. Above we have implemented this by means of an association
+  list. Replay the development replacing \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie{\isacharparenright}\ list}
+  with \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ option}.
+\end{exercise}%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables: