diff -r a99747ccba87 -r 9a9cc62932d9 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jun 12 14:20:25 2008 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jun 12 14:20:52 2008 +0200
@@ -179,7 +179,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}n{\isacharasterisk}n\ {\isacharequal}\ n{\isacharplus}{\isadigit{1}}\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}{\isachardoublequoteclose}%
 \isadelimproof
 %
 \endisadelimproof
@@ -195,9 +195,9 @@
 %
 \begin{isamarkuptext}%
 \noindent
-is not proved even by \isa{arith} because the proof relies 
+is not proved by \isa{arith} because the proof relies 
 on properties of multiplication. Only multiplication by numerals (which is
-the same as iterated addition) is allowed.
+the same as iterated addition) is taken into account.
 
 \begin{warn} The running time of \isa{arith} is exponential in the number
   of occurrences of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and