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