1.1 --- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Fri Sep 01 18:29:52 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/document/asm_simp.tex	Fri Sep 01 19:09:44 2000 +0200
     1.3 @@ -9,9 +9,9 @@
     1.4  \isacommand{by}\ simp%
     1.5  \begin{isamarkuptext}%
     1.6  \noindent
     1.7 -The second assumption simplifies to \isa{\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
     1.8 -simplifies the first assumption to \isa{\mbox{zs}\ {\isacharequal}\ \mbox{ys}}, thus reducing the
     1.9 -conclusion to \isa{\mbox{ys}\ {\isacharequal}\ \mbox{ys}} and hence to \isa{True}.
    1.10 +The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
    1.11 +simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the
    1.12 +conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}.
    1.13  
    1.14  In some cases this may be too much of a good thing and may lead to
    1.15  nontermination:%
    1.16 @@ -20,7 +20,7 @@
    1.17  \begin{isamarkuptxt}%
    1.18  \noindent
    1.19  cannot be solved by an unmodified application of \isa{simp} because the
    1.20 -simplification rule \isa{\mbox{f}\ \mbox{x}\ {\isacharequal}\ \mbox{g}\ {\isacharparenleft}\mbox{f}\ {\isacharparenleft}\mbox{g}\ \mbox{x}{\isacharparenright}{\isacharparenright}} extracted from the assumption
    1.21 +simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}} extracted from the assumption
    1.22  does not terminate. Isabelle notices certain simple forms of
    1.23  nontermination but not this one. The problem can be circumvented by
    1.24  explicitly telling the simplifier to ignore the assumptions:%
    1.25 @@ -30,17 +30,17 @@
    1.26  \noindent
    1.27  There are three options that influence the treatment of assumptions:
    1.28  \begin{description}
    1.29 -\item[\isa{(no_asm)}]\indexbold{*no_asm}
    1.30 +\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
    1.31   means that assumptions are completely ignored.
    1.32 -\item[\isa{(no_asm_simp)}]\indexbold{*no_asm_simp}
    1.33 +\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp}
    1.34   means that the assumptions are not simplified but
    1.35    are used in the simplification of the conclusion.
    1.36 -\item[\isa{(no_asm_use)}]\indexbold{*no_asm_use}
    1.37 +\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use}
    1.38   means that the assumptions are simplified but are not
    1.39    used in the simplification of each other or the conclusion.
    1.40  \end{description}
    1.41 -Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above
    1.42 -problematic subgoal.
    1.43 +Neither \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} nor \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} allow to simplify
    1.44 +the above problematic subgoal.
    1.45  
    1.46  Note that only one of the above options is allowed, and it must precede all
    1.47  other arguments.%