| author | wenzelm |
| Tue, 01 Aug 2000 13:43:22 +0200 | |
| changeset 9490 | c2606af9922c |
| parent 9458 | c613cd06d5cf |
| child 9541 | d17c0b34d5c8 |
| permissions | -rw-r--r-- |
| 8749 | 1 |
\begin{isabelle}%
|
2 |
\isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline
|
|
| 9458 | 3 |
\isacommand{by}(simp~add:~Let\_def)%
|
| 8749 | 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: |