doc-src/TutorialI/Inductive/Even.thy

--- a/doc-src/TutorialI/Inductive/Even.thy	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Even.thy	Thu Nov 29 14:12:42 2001 +0100
@@ -21,7 +21,7 @@
 
 Our first lemma states that numbers of the form $2\times k$ are even. *}
 lemma two_times_even[intro!]: "2*k \<in> even"
-apply (induct "k")
+apply (induct_tac k)
 txt{*
 The first step is induction on the natural number \isa{k}, which leaves
 two subgoals: