| author | paulson |
| Wed, 28 Jun 2000 10:57:35 +0200 | |
| changeset 9174 | 6ef054f33f83 |
| parent 8771 | 026f37a86ea7 |
| child 9458 | c613cd06d5cf |
| permissions | -rw-r--r-- |
| 8745 | 1 |
(*<*) |
2 |
theory let_rewr = Main:; |
|
3 |
(*>*) |
|
4 |
lemma "(let xs = [] in xs@ys@xs) = ys"; |
|
5 |
apply(simp add: Let_def).; |
|
6 |
||
7 |
text{*
|
|
8 |
If, in a particular context, there is no danger of a combinatorial explosion |
|
| 8771 | 9 |
of nested \isa{let}s one could even add \isa{Let_def} permanently:
|
| 8745 | 10 |
*} |
11 |
theorems [simp] = Let_def; |
|
12 |
(*<*) |
|
13 |
end |
|
14 |
(*>*) |