| changeset 9541 | d17c0b34d5c8 |
| parent 9145 | 9f7b8de5bfaf |
| child 9673 | 1b2d4f995b13 |
--- a/doc-src/TutorialI/Misc/document/arith3.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith3.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{lemma}~{"}n*n~=~n~{\isasymLongrightarrow}~n=0~{\isasymor}~n=1{"}\isanewline +\isacommand{lemma}\ {"}n*n\ =\ n\ {\isasymLongrightarrow}\ n=0\ {\isasymor}\ n=1{"}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex