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