--- a/doc-src/TutorialI/Misc/document/Plus.tex Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Plus.tex Wed Jan 29 16:29:38 2003 +0100
@@ -20,8 +20,7 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%