doc-src/TutorialI/Misc/document/arith1.tex
changeset 9717 699de91b15e2
parent 9673 1b2d4f995b13
child 9721 7e51c9f3d5a0
equal deleted inserted replaced
9716:9be481b4bc85 9717:699de91b15e2
     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: