
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/Inductive/even-example.tex
--- 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}




