doc-src/TutorialI/Misc/document/simp.tex
changeset 10971 6852682eaf16
parent 10950 aa788fcb75a5
child 10983 59961d32b1ae
     1.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4  where the list of \emph{modifiers} fine tunes the behaviour and may
     1.5  be empty. Most if not all of the proofs seen so far could have been performed
     1.6  with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
     1.7 -only the first subgoal and may thus need to be repeated---use
     1.8 +only the first subgoal and may thus need to be repeated --- use
     1.9  \isaindex{simp_all} to simplify all subgoals.
    1.10  Note that \isa{simp} fails if nothing changes.%
    1.11  \end{isamarkuptext}%
    1.12 @@ -109,7 +109,7 @@
    1.13  \isacommand{done}%
    1.14  \begin{isamarkuptext}%
    1.15  \noindent
    1.16 -There are three options that influence the treatment of assumptions:
    1.17 +There are three modifiers that influence the treatment of assumptions:
    1.18  \begin{description}
    1.19  \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
    1.20   means that assumptions are completely ignored.
    1.21 @@ -122,7 +122,7 @@
    1.22  \end{description}
    1.23  Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on
    1.24  the problematic subgoal above.
    1.25 -Note that only one of the options is allowed, and it must precede all
    1.26 +Note that only one of the modifiers is allowed, and it must precede all
    1.27  other arguments.%
    1.28  \end{isamarkuptext}%
    1.29  %
    1.30 @@ -169,13 +169,14 @@
    1.31  rule because this defeats the whole purpose of an abbreviation.
    1.32  
    1.33  \begin{warn}
    1.34 -  If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
    1.35 -  occurrences of $f$ with at least two arguments. Thus it is safer to define
    1.36 -  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
    1.37 +  If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
    1.38 +  occurrences of $f$ with at least two arguments. This may be helpful for unfolding
    1.39 +  $f$ selectively, but it may also get in the way. Defining
    1.40 +  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
    1.41  \end{warn}%
    1.42  \end{isamarkuptext}%
    1.43  %
    1.44 -\isamarkupsubsubsection{Simplifying Let-Expressions%
    1.45 +\isamarkupsubsubsection{Simplifying {\tt\slshape let}-Expressions%
    1.46  }
    1.47  %
    1.48  \begin{isamarkuptext}%
    1.49 @@ -360,7 +361,7 @@
    1.50  Applying instance of rewrite rule:
    1.51  rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
    1.52  Rewriting:
    1.53 -rev [x] == rev [] @ [x]
    1.54 +rev [a] == rev [] @ [a]
    1.55  Applying instance of rewrite rule:
    1.56  rev [] == []
    1.57  Rewriting:
    1.58 @@ -368,11 +369,11 @@
    1.59  Applying instance of rewrite rule:
    1.60  [] @ ?y == ?y
    1.61  Rewriting:
    1.62 -[] @ [x] == [x]
    1.63 +[] @ [a] == [a]
    1.64  Applying instance of rewrite rule:
    1.65  ?x3 \# ?t3 = ?t3 == False
    1.66  Rewriting:
    1.67 -[x] = [] == False
    1.68 +[a] = [] == False
    1.69  \end{ttbox}
    1.70  
    1.71  In more complicated cases, the trace can be quite lenghty, especially since