--- a/doc-src/TutorialI/Misc/document/def_rewr.tex Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-%
-\begin{isabellebody}%
-%
-\begin{isamarkuptext}%
-\noindent Constant definitions (\S\ref{sec:ConstDefinitions}) can
-be used as simplification rules, but by default they are not. Hence the
-simplifier does not expand them automatically, just as it should be:
-definitions are introduced for the purpose of abbreviating complex
-concepts. Of course we need to expand the definitions initially to derive
-enough lemmas that characterize the concept sufficiently for us to forget the
-original definition. For example, given%
-\end{isamarkuptext}%
-\isacommand{constdefs}\ exor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}%
-\begin{isamarkuptext}%
-\noindent
-we may want to prove%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}exor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
-\begin{isamarkuptxt}%
-\noindent
-Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
-get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
-\end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}exor{\isacharunderscore}def{\isacharparenright}%
-\begin{isamarkuptxt}%
-\noindent
-In this particular case, the resulting goal
-\begin{isabelle}
-~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
-\end{isabelle}
-can be proved by simplification. Thus we could have proved the lemma outright%
-\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-Of course we can also unfold definitions in the middle of a proof.
-
-You should normally not turn a definition permanently into a simplification
-rule because this defeats the whole purpose of an abbreviation.%
-\end{isamarkuptext}%
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: