1.1 --- a/doc-src/TutorialI/Recdef/Induction.thy	Mon Oct 09 09:33:45 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Mon Oct 09 10:18:21 2000 +0200
     1.3 @@ -41,7 +41,8 @@
     1.4  The rest is pure simplification:
     1.5  *}
     1.6  
     1.7 -by simp_all;
     1.8 +apply simp_all;
     1.9 +done
    1.10  
    1.11  text{*
    1.12  Try proving the above lemma by structural induction, and you find that you