# HG changeset patch
# User paulson
# Date 990091868 -7200
# Node ID f0661da2f6ae1de76a4ecd51c982f3b4fef80a2a
# Parent  9e0708bb15f78bdd62e9d3723c662053ef25d219
typo, etc.

diff -r 9e0708bb15f7 -r f0661da2f6ae doc-src/TutorialI/Trie/Trie.thy
--- 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}