--- a/doc-src/TutorialI/Misc/document/let_rewr.tex Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-%
-\begin{isabellebody}%
-%
-\isamarkupsubsubsection{Simplifying let-expressions}
-%
-\begin{isamarkuptext}%
-\index{simplification!of let-expressions}
-Proving a goal containing \isaindex{let}-expressions almost invariably
-requires the \isa{let}-con\-structs to be expanded at some point. Since
-\isa{let}-\isa{in} is just syntactic sugar for a predefined constant
-(called \isa{Let}), expanding \isa{let}-constructs means rewriting with
-\isa{Let{\isacharunderscore}def}:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
-\begin{isamarkuptext}%
-If, in a particular context, there is no danger of a combinatorial explosion
-of nested \isa{let}s one could even add \isa{Let{\isacharunderscore}def} permanently:%
-\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: