--- 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