changeset 8745 | 13b32661dde4 |
child 8771 | 026f37a86ea7 |
8744:22fa8b16c3ae | 8745:13b32661dde4 |
---|---|
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 |
|
9 of nested \texttt{let}s one could even add \texttt{Let_def} permanently: |
|
10 *} |
|
11 theorems [simp] = Let_def; |
|
12 (*<*) |
|
13 end |
|
14 (*>*) |