diff -r d1415164b814 -r 751fde5307e4 doc-src/TutorialI/Trie/Trie.thy
--- a/doc-src/TutorialI/Trie/Trie.thy	Fri Aug 25 12:17:09 2000 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy	Mon Aug 28 09:32:51 2000 +0200
@@ -52,7 +52,7 @@
 *};
 
 lemma [simp]: "lookup (Trie None []) as = None";
-by(case_tac as, auto);
+by(case_tac as, simp_all);
 
 text{*
 Things begin to get interesting with the definition of an update function
@@ -129,8 +129,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.
 *};