doc-src/TutorialI/Misc/Itrev.thy

--- a/doc-src/TutorialI/Misc/Itrev.thy	Fri Aug 25 12:17:09 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Mon Aug 28 09:32:51 2000 +0200
@@ -28,7 +28,7 @@
 There is no choice as to the induction variable, and we immediately simplify:
 *};
 
-apply(induct_tac xs, auto);
+apply(induct_tac xs, simp_all);
 
 txt{*\noindent
 Unfortunately, this is not a complete success:
@@ -94,6 +94,6 @@
 *};
 
 (*<*)
-by(induct_tac xs, simp, simp);
+by(induct_tac xs, simp_all);
 end
 (*>*)