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