--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Jul 28 16:02:51 2000 +0200
@@ -105,7 +105,7 @@
that contains two \isa{case}-expressions over instructions. Thus we add
automatic case splitting as well, which finishes the proof:
*}
-apply(induct_tac xs, simp, simp split: instr.split).;
+by(induct_tac xs, simp, simp split: instr.split);
text{*\noindent
Note that because \isaindex{auto} performs simplification, it can
@@ -116,7 +116,7 @@
lemmas [simp del] = exec_app;
lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)";
(*>*)
-apply(induct_tac xs, auto split: instr.split).;
+by(induct_tac xs, auto split: instr.split);
text{*\noindent
Although this is more compact, it is less clear for the reader of the proof.
@@ -128,6 +128,6 @@
*}
(*<*)
theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
-apply(induct_tac e, auto).;
+by(induct_tac e, auto);
end
(*>*)