diff -r c5fc121c2067 -r f0740137a65d doc-src/TutorialI/Trie/document/Trie.tex
--- a/doc-src/TutorialI/Trie/document/Trie.tex	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -44,7 +44,7 @@
 distinguishes the two cases whether the search string is empty or not:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}lookup\ {\isacharparenleft}Trie\ None\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ as\ {\isacharequal}\ None{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ auto{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
 \begin{isamarkuptext}%
 Things begin to get interesting with the definition of an update function
 that adds a new (string,value) pair to a trie, overwriting the old value
@@ -117,8 +117,8 @@
 This proof may look surprisingly straightforward. However, note that this
 comes at a cost: the proof script is unreadable because the
 intermediate proof states are invisible, and we rely on the (possibly
-brittle) magic of \isa{auto} (after the induction) to split the remaining
-goals up in such a way that case distinction on \isa{bs} makes sense and
+brittle) magic of \isa{auto} (\isa{simp\_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. Part~\ref{Isar} shows you how to write readable and stable
 proofs.%
 \end{isamarkuptext}%