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