diff -r 2d4433759b8d -r 37636be4cbd1 doc-src/TutorialI/Misc/natsum.thy
--- 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}
 *}