--- a/doc-src/TutorialI/Inductive/AB.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy Thu Nov 29 21:12:37 2001 +0100
@@ -132,7 +132,7 @@
discuss it.
*}
-apply(induct w)
+apply(induct_tac w)
apply(simp)
by(force simp add: zabs_def take_Cons split: nat.split if_splits)