# HG changeset patch
# User nipkow
# Date 1213273252 -7200
# Node ID 9a9cc62932d97db20de1d688258c94c168af31c2
# Parent  a99747ccba87b1c7284d7f051d2828320ec33f3e
lemma modified

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
diff -r a99747ccba87 -r 9a9cc62932d9 doc-src/TutorialI/Misc/natsum.thy
--- 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