diff -r 140f1e0ea846 -r 6109d4020420 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Wed Jul 13 15:06:20 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Wed Jul 13 15:19:13 2005 +0200
@@ -91,7 +91,7 @@
 \begin{isamarkuptext}%
 \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, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -135,7 +135,7 @@
 \isa{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, \isa{arith} may take
+If the formula involves quantifiers, \isa{arith} may take
 super-exponential time and space.
 \end{warn}%
 \end{isamarkuptext}%