equal
deleted
inserted
replaced
4 lemma "(let xs = [] in xs@ys@xs) = ys"; |
4 lemma "(let xs = [] in xs@ys@xs) = ys"; |
5 apply(simp add: Let_def).; |
5 apply(simp add: Let_def).; |
6 |
6 |
7 text{* |
7 text{* |
8 If, in a particular context, there is no danger of a combinatorial explosion |
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: |
9 of nested \isa{let}s one could even add \isa{Let_def} permanently: |
10 *} |
10 *} |
11 theorems [simp] = Let_def; |
11 theorems [simp] = Let_def; |
12 (*<*) |
12 (*<*) |
13 end |
13 end |
14 (*>*) |
14 (*>*) |