diff -r cc8aa63bdad6 -r 8016321c7de1 doc-src/TutorialI/Misc/document/asm_simp.tex
--- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-%
-\begin{isabellebody}%
-%
-\begin{isamarkuptext}%
-By default, assumptions are part of the simplification process: they are used
-as simplification rules and are simplified themselves. For example:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ xs\ {\isacharat}\ zs\ {\isacharequal}\ ys\ {\isacharat}\ xs{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ zs{\isachardoublequote}\isanewline
-\isacommand{by}\ simp%
-\begin{isamarkuptext}%
-\noindent
-The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
-simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the
-conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}.
-
-In some cases this may be too much of a good thing and may lead to
-nontermination:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
-\begin{isamarkuptxt}%
-\noindent
-cannot be solved by an unmodified application of \isa{simp} because the
-simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}} extracted from the assumption
-does not terminate. Isabelle notices certain simple forms of
-nontermination but not this one. The problem can be circumvented by
-explicitly telling the simplifier to ignore the assumptions:%
-\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-There are three options that influence the treatment of assumptions:
-\begin{description}
-\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
- means that assumptions are completely ignored.
-\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp}
- means that the assumptions are not simplified but
-  are used in the simplification of the conclusion.
-\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use}
- means that the assumptions are simplified but are not
-  used in the simplification of each other or the conclusion.
-\end{description}
-Neither \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} nor \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} allow to simplify
-the above problematic subgoal.
-
-Note that only one of the above options is allowed, and it must precede all
-other arguments.%
-\end{isamarkuptext}%
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: