author | nipkow |
Tue, 25 Apr 2000 08:09:10 +0200 | |
changeset 8771 | 026f37a86ea7 |
parent 8745 | 13b32661dde4 |
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 |
(*>*) |