--- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Mon Oct 09 10:18:21 2000 +0200
@@ -19,7 +19,8 @@
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
+\isacommand{done}\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex