equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 \begin{isabelle}% |
2 \isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline |
2 \isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline |
3 \isacommand{apply}(simp~add:~Let\_def)\isacommand{.}% |
3 \isacommand{apply}(simp~add:~Let\_def)\isacommand{.}% |
4 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
5 If, in a particular context, there is no danger of a combinatorial explosion |
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:% |
6 of nested \isa{let}s one could even add \isa{Let_def} permanently:% |
7 \end{isamarkuptext}% |
7 \end{isamarkuptext}% |
8 \isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}% |
8 \isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}% |