--- a/doc-src/TutorialI/Misc/document/natsum.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Tue Dec 17 11:05:41 2002 +0100
@@ -132,6 +132,7 @@
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables: