--- a/doc-src/TutorialI/Misc/natsum.thy Mon Jul 11 16:42:42 2005 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Mon Jul 11 19:59:11 2005 +0200
@@ -80,7 +80,7 @@
text{*\noindent
For efficiency's sake, this built-in prover ignores quantified formulae,
-logical connectives, and all arithmetic operations apart from addition.
+many logical connectives, and all arithmetic operations apart from addition.
In consequence, @{text auto} and @{text simp} cannot prove this slightly more complex goal:
*}
@@ -119,7 +119,7 @@
@{text k}~\sdx{dvd} are also supported, where the former two are eliminated
by case distinctions, again blowing up the running time.
-If the formula involves explicit quantifiers, @{text arith} may take
+If the formula involves quantifiers, @{text arith} may take
super-exponential time and space.
\end{warn}
*}