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