doc-src/TutorialI/CodeGen/document/CodeGen.tex
changeset 10971 6852682eaf16
parent 10878 b254d5ad6dd4
child 11428 332347b9b942
     1.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4  \isa{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  \end{isamarkuptext}%
    1.11  \isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v\ list\ {\isasymRightarrow}\ {\isacharprime}v\ list{\isachardoublequote}\isanewline
    1.12 @@ -102,11 +102,11 @@
    1.13  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
    1.14  \begin{isamarkuptext}%
    1.15  \noindent
    1.16 -Note that because \isaindex{auto} performs simplification, it can
    1.17 -also be modified in the same way \isa{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 \isa{simp} can. Thus the proof can be
    1.20  rewritten as%
    1.21  \end{isamarkuptext}%
    1.22 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
    1.23 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
    1.24  \begin{isamarkuptext}%
    1.25  \noindent
    1.26  Although this is more compact, it is less clear for the reader of the proof.