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