
diff -r 279da0358aa9 -r 09a6c44a48ea doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Fri Aug 03 18:04:55 2001 +0200
@@ -70,9 +70,13 @@
 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-For efficiency's sake, this built-in prover ignores quantified formulae and all 
-arithmetic operations apart from addition.
-
+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:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
 The method \methdx{arith} is more general.  It attempts to prove
 the first subgoal provided it is a quantifier-free \textbf{linear arithmetic}
 formula.  Such formulas may involve the




