--- a/doc-src/TutorialI/Trie/document/Trie.tex Thu May 17 11:31:08 2001 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Thu May 17 11:31:21 2001 +0200
@@ -127,10 +127,10 @@
\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.
+ deletion of entries with a single function. Prove the corresponding version
+ of the main theorem above.
+ Optimize your function such that it shrinks tries after
+ deletion if possible.
\end{exercise}
\begin{exercise}