typo, etc.

--- a/doc-src/TutorialI/Trie/Trie.thy	Thu May 17 11:29:04 2001 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy	Thu May 17 11:31:08 2001 +0200
@@ -137,10 +137,10 @@
 
 \begin{exercise}
   Modify @{term 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}