doc-src/TutorialI/CodeGen/CodeGen.thy
 changeset 10971 6852682eaf16 parent 10885 90695f46440b child 11428 332347b9b942
     1.1 --- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Wed Jan 24 11:59:15 2001 +0100
1.2 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Wed Jan 24 12:29:10 2001 +0100
1.3 @@ -49,7 +49,7 @@
1.4  @{text"exec"} that takes a list of instructions, a store (modelled as a
1.5  function from addresses to values, just like the environment for
1.6  evaluating expressions), and a stack (modelled as a list) of values,
1.7 -and returns the stack at the end of the execution---the store remains
1.8 +and returns the stack at the end of the execution --- the store remains
1.9  unchanged:
1.10  *}
1.11
1.12 @@ -110,15 +110,15 @@
1.13  apply(induct_tac xs, simp, simp split: instr.split);
1.14  (*<*)done(*>*)
1.15  text{*\noindent
1.16 -Note that because \isaindex{auto} performs simplification, it can
1.17 -also be modified in the same way @{text simp} can. Thus the proof can be
1.18 +Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
1.19 +be modified in the same way @{text simp} can. Thus the proof can be
1.20  rewritten as
1.21  *}
1.22  (*<*)
1.23  declare exec_app[simp del];
1.24  lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)";
1.25  (*>*)
1.26 -apply(induct_tac xs, auto split: instr.split);
1.27 +apply(induct_tac xs, simp_all split: instr.split);
1.28  (*<*)done(*>*)
1.29  text{*\noindent
1.30  Although this is more compact, it is less clear for the reader of the proof.