| changeset 10538 | d1bf9ca9008d |
| parent 10537 | 1d2f15504d38 |
| child 10539 | 5929460a41df |
| 10537:1d2f15504d38 | 10538:d1bf9ca9008d |
|---|---|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{arith{\isadigit{1}}}% |
|
4 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline |
|
5 \end{isabellebody}% |
|
6 %%% Local Variables: |
|
7 %%% mode: latex |
|
8 %%% TeX-master: "root" |
|
9 %%% End: |