--- a/doc-src/TutorialI/Misc/natsum.thy Thu Jul 26 16:43:02 2001 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy 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 (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
@{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},
and the operations