# HG changeset patch
# User nipkow
# Date 1022512816 -7200
# Node ID dc393bbee6cefce5380b8c7f2a007e2daac3c9e2
# Parent  a82610e49b2d9ec9eb8fe079820d527b5a152d58
*** empty log message ***

diff -r a82610e49b2d -r dc393bbee6ce doc-src/TutorialI/Misc/document/natsum.tex
--- 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}%
diff -r a82610e49b2d -r dc393bbee6ce doc-src/TutorialI/Misc/natsum.thy
--- 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