diff -r 279da0358aa9 -r 09a6c44a48ea doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Fri Aug 03 18:04:55 2001 +0200
@@ -70,9 +70,15 @@
 (*<*)by(auto)(*>*)
 
 text{*\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, @{text auto} cannot prove this slightly more complex goal:
+*}
 
+lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
+(*<*)by(arith)(*>*)
+
+text{*\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