diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/arith3.tex
--- 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