doc-src/TutorialI/Misc/document/arith3.tex
changeset 9673 1b2d4f995b13
parent 9541 d17c0b34d5c8
child 9717 699de91b15e2
equal deleted inserted replaced
9672:2c208c98f541 9673:1b2d4f995b13
     1 \begin{isabelle}%
     1 \begin{isabelle}%
     2 \isacommand{lemma}\ {"}n*n\ =\ n\ {\isasymLongrightarrow}\ n=0\ {\isasymor}\ n=1{"}\isanewline
     2 \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}\isadigit{0}\ {\isasymor}\ n{\isacharequal}\isadigit{1}{\isachardoublequote}\isanewline
     3 \end{isabelle}%
     3 \end{isabelle}%
     4 %%% Local Variables:
     4 %%% Local Variables:
     5 %%% mode: latex
     5 %%% mode: latex
     6 %%% TeX-master: "root"
     6 %%% TeX-master: "root"
     7 %%% End:
     7 %%% End: