diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -18,7 +18,7 @@
 \end{isamarkuptext}%
 \isacommand{lemma}~{"}sum~n~+~sum~n~=~n*(Suc~n){"}\isanewline
 \isacommand{apply}(induct\_tac~n)\isanewline
-\isacommand{apply}(auto)\isacommand{.}\isanewline
+\isacommand{by}(auto)\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex