| author | wenzelm |
| Tue, 27 Jun 2000 20:35:31 +0200 | |
| changeset 9155 | adfa40218e06 |
| parent 9145 | 9f7b8de5bfaf |
| child 9458 | c613cd06d5cf |
| permissions | -rw-r--r-- |
| 8749 | 1 |
\begin{isabelle}%
|
2 |
\isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline
|
|
3 |
\isacommand{apply}(simp~add:~Let\_def)\isacommand{.}%
|
|
4 |
\begin{isamarkuptext}%
|
|
5 |
If, in a particular context, there is no danger of a combinatorial explosion |
|
| 8771 | 6 |
of nested \isa{let}s one could even add \isa{Let_def} permanently:%
|
| 8749 | 7 |
\end{isamarkuptext}%
|
8 |
\isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}%
|
|
| 9145 | 9 |
%%% Local Variables: |
10 |
%%% mode: latex |
|
11 |
%%% TeX-master: "root" |
|
12 |
%%% End: |