| changeset 12328 | 7c4ec77a8715 |
| parent 11494 | 23a118849801 |
| child 12663 | d33033205e2f |
--- a/doc-src/TutorialI/Inductive/even-example.tex Thu Nov 29 13:33:45 2001 +0100 +++ b/doc-src/TutorialI/Inductive/even-example.tex Thu Nov 29 14:12:42 2001 +0100 @@ -59,7 +59,7 @@ \begin{isabelle} \isacommand{lemma}\ two_times_even[intro!]:\ "\#2*k\ \isasymin \ even" \isanewline -\isacommand{apply}\ (induct\ "k")\isanewline +\isacommand{apply}\ (induct_tac\ k)\isanewline \ \isacommand{apply}\ auto\isanewline \isacommand{done} \end{isabelle}