
diff -r dfff821d2949 -r 59d6633835fa doc-src/TutorialI/Recdef/document/Induction.tex
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -38,7 +38,8 @@
 \end{isabelle}
 The rest is pure simplification:%
 \end{isamarkuptxt}%
-\isacommand{by}\ simp{\isacharunderscore}all%
+\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 Try proving the above lemma by structural induction, and you find that you
 need an additional case distinction. What is worse, the names of variables




