--- a/doc-src/TutorialI/Misc/document/simp.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Jan 24 12:29:10 2001 +0100
@@ -52,7 +52,7 @@
where the list of \emph{modifiers} fine tunes the behaviour and may
be empty. Most if not all of the proofs seen so far could have been performed
with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
-only the first subgoal and may thus need to be repeated---use
+only the first subgoal and may thus need to be repeated --- use
\isaindex{simp_all} to simplify all subgoals.
Note that \isa{simp} fails if nothing changes.%
\end{isamarkuptext}%
@@ -109,7 +109,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-There are three options that influence the treatment of assumptions:
+There are three modifiers that influence the treatment of assumptions:
\begin{description}
\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
means that assumptions are completely ignored.
@@ -122,7 +122,7 @@
\end{description}
Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on
the problematic subgoal above.
-Note that only one of the options is allowed, and it must precede all
+Note that only one of the modifiers is allowed, and it must precede all
other arguments.%
\end{isamarkuptext}%
%
@@ -169,13 +169,14 @@
rule because this defeats the whole purpose of an abbreviation.
\begin{warn}
- If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
- occurrences of $f$ with at least two arguments. Thus it is safer to define
- $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
+ If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
+ occurrences of $f$ with at least two arguments. This may be helpful for unfolding
+ $f$ selectively, but it may also get in the way. Defining
+ $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Simplifying Let-Expressions%
+\isamarkupsubsubsection{Simplifying {\tt\slshape let}-Expressions%
}
%
\begin{isamarkuptext}%
@@ -360,7 +361,7 @@
Applying instance of rewrite rule:
rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
Rewriting:
-rev [x] == rev [] @ [x]
+rev [a] == rev [] @ [a]
Applying instance of rewrite rule:
rev [] == []
Rewriting:
@@ -368,11 +369,11 @@
Applying instance of rewrite rule:
[] @ ?y == ?y
Rewriting:
-[] @ [x] == [x]
+[] @ [a] == [a]
Applying instance of rewrite rule:
?x3 \# ?t3 = ?t3 == False
Rewriting:
-[x] = [] == False
+[a] = [] == False
\end{ttbox}
In more complicated cases, the trace can be quite lenghty, especially since