diff -r 7eb63f63e6c6 -r 279da0358aa9 doc-src/TutorialI/Misc/natsum.thy
--- 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