diff -r 7eb63f63e6c6 -r 279da0358aa9 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jul 26 16:43:02 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jul 26 18:23:38 2001 +0200
@@ -74,8 +74,8 @@
 arithmetic operations apart from addition.
 
 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
+the first subgoal provided it is a quantifier-free \textbf{linear arithmetic}
+formula.  Such formulas may involve the
 usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
 \isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
 and the operations