doc-src/TutorialI/Misc/document/let_rewr.tex

begin_theory: store *copy* of initial theory;

\begin{isabelle}%
\isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline
\isacommand{apply}(simp~add:~Let\_def)\isacommand{.}%
\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_def} permanently:%
\end{isamarkuptext}%
\isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: