1.1 --- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Fri Jul 28 13:04:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Fri Jul 28 16:02:51 2000 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  that contains two \isa{case}-expressions over instructions. Thus we add
     1.5  automatic case splitting as well, which finishes the proof:
     1.6  *}
     1.7 -apply(induct_tac xs, simp, simp split: instr.split).;
     1.8 +by(induct_tac xs, simp, simp split: instr.split);
     1.9  
    1.10  text{*\noindent
    1.11  Note that because \isaindex{auto} performs simplification, it can
    1.12 @@ -116,7 +116,7 @@
    1.13  lemmas [simp del] = exec_app;
    1.14  lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    1.15  (*>*)
    1.16 -apply(induct_tac xs, auto split: instr.split).;
    1.17 +by(induct_tac xs, auto split: instr.split);
    1.18  
    1.19  text{*\noindent
    1.20  Although this is more compact, it is less clear for the reader of the proof.
    1.21 @@ -128,6 +128,6 @@
    1.22  *}
    1.23  (*<*)
    1.24  theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
    1.25 -apply(induct_tac e, auto).;
    1.26 +by(induct_tac e, auto);
    1.27  end
    1.28  (*>*)