diff -r dfff821d2949 -r 59d6633835fa doc-src/TutorialI/Recdef/Induction.thy
--- a/doc-src/TutorialI/Recdef/Induction.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Induction.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -41,7 +41,8 @@
 The rest is pure simplification:
 *}
 
-by simp_all;
+apply simp_all;
+done
 
 text{*
 Try proving the above lemma by structural induction, and you find that you