doc-src/TutorialI/Misc/document/arith1.tex
changeset 9722 a5f86aed785b
parent 9721 7e51c9f3d5a0
child 9924 3370f6aa3200
equal deleted inserted replaced
9721:7e51c9f3d5a0 9722:a5f86aed785b
     1 \begin{isabelle}%
     1 %
       
     2 \begin{isabellebody}%
     2 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
     3 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
     3 \end{isabelle}%
     4 \end{isabellebody}%
     4 %%% Local Variables:
     5 %%% Local Variables:
     5 %%% mode: latex
     6 %%% mode: latex
     6 %%% TeX-master: "root"
     7 %%% TeX-master: "root"
     7 %%% End:
     8 %%% End: