| changeset 8749 | 2665170f104a |
| child 8771 | 026f37a86ea7 |
| 8748:cb9d47632573 | 8749:2665170f104a |
|---|---|
1 \begin{isabelle}% |
|
2 \isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline |
|
3 \isacommand{apply}(simp~add:~Let\_def)\isacommand{.}% |
|
4 \begin{isamarkuptext}% |
|
5 If, in a particular context, there is no danger of a combinatorial explosion |
|
6 of nested \texttt{let}s one could even add \texttt{Let_def} permanently:% |
|
7 \end{isamarkuptext}% |
|
8 \isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}% |