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.