equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline |
3 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline |
3 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% |
4 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% |
4 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
5 If, in a particular context, there is no danger of a combinatorial explosion |
6 If, in a particular context, there is no danger of a combinatorial explosion |
6 of nested \isa{let}s one could even add \isa{Let_def} permanently:% |
7 of nested \isa{let}s one could even add \isa{Let_def} permanently:% |
7 \end{isamarkuptext}% |
8 \end{isamarkuptext}% |
8 \isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabelle}% |
9 \isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabellebody}% |
9 %%% Local Variables: |
10 %%% Local Variables: |
10 %%% mode: latex |
11 %%% mode: latex |
11 %%% TeX-master: "root" |
12 %%% TeX-master: "root" |
12 %%% End: |
13 %%% End: |