doc-src/TutorialI/Recdef/document/Induction.tex
changeset 9458 c613cd06d5cf
parent 9145 9f7b8de5bfaf
child 9541 d17c0b34d5c8
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -36,7 +36,7 @@
 \end{isabellepar}%
 The rest is pure simplification:%
 \end{isamarkuptxt}%
-\isacommand{apply}~auto\isacommand{.}%
+\isacommand{by}~auto%
 \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