--- 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
--- a/doc-src/TutorialI/Misc/natsum.thy Thu Jun 12 14:20:25 2008 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Thu Jun 12 14:20:52 2008 +0200
@@ -103,13 +103,13 @@
succeeds because @{term"k*k"} can be treated as atomic. In contrast,
*}
-lemma "n*n = n \<Longrightarrow> n=0 \<or> n=1"
+lemma "n*n = n+1 \<Longrightarrow> n=0"
(*<*)oops(*>*)
text{*\noindent
-is not proved even by @{text arith} because the proof relies
+is not proved by @{text 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 @{text arith} is exponential in the number
of occurrences of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and