*** empty log message ***

--- a/doc-src/TutorialI/Misc/document/natsum.tex	Fri May 24 16:56:25 2002 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon May 27 17:20:16 2002 +0200
@@ -85,10 +85,10 @@
 \noindent
 For efficiency's sake, this built-in prover ignores quantified formulae,
 logical connectives, and all arithmetic operations apart from addition.
-In consequence, \isa{auto} cannot prove this slightly more complex goal:%
+In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Misc/natsum.thy	Fri May 24 16:56:25 2002 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Mon May 27 17:20:16 2002 +0200
@@ -75,10 +75,10 @@
 text{*\noindent
 For efficiency's sake, this built-in prover ignores quantified formulae,
 logical connectives, and all arithmetic operations apart from addition.
-In consequence, @{text auto} cannot prove this slightly more complex goal:
+In consequence, @{text auto} and @{text simp} cannot prove this slightly more complex goal:
 *}
 
-lemma "\<not> m < n \<and> m < n + (1::nat) \<Longrightarrow> m = n";
+lemma "m \<noteq> (n::nat) \<Longrightarrow> m < n \<or> n < m"
 (*<*)by(arith)(*>*)
 
 text{*\noindent