diff -r 55f33da63366 -r 458068404143 doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Wed Dec 13 09:32:55 2000 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy	Wed Dec 13 09:39:53 2000 +0100
@@ -27,7 +27,8 @@
 \isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
 \isaindexbold{max} are predefined, as are the relations
 \indexboldpos{\isasymle}{$HOL2arithrel} and
-\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
+\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if
+@{prop"m<n"}. There is even a least number operation
 \isaindexbold{LEAST}. For example, @{prop"(LEAST n. 1 < n) = 2"}, although
 Isabelle does not prove this completely automatically. Note that @{term 1}
 and @{term 2} are available as abbreviations for the corresponding
@@ -69,7 +70,9 @@
 (which attacks the first subgoal). It proves arithmetic goals involving the
 usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
 @{text"\<longrightarrow>"}), the relations @{text"\<le>"} and @{text"<"}, and the operations
-@{text"+"}, @{text"-"}, @{term min} and @{term max}. For example,
+@{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
+known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
+For example,
 *}
 
 lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
@@ -92,8 +95,8 @@
   of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
   \isaindexbold{max} because they are first eliminated by case distinctions.
 
-  \isa{arith} is incomplete even for the restricted class of formulae
-  described above (known as ``linear arithmetic''). If divisibility plays a
+  \isa{arith} is incomplete even for the restricted class of
+  linear arithmetic formulae. If divisibility plays a
   role, it may fail to prove a valid formula, for example
   @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare in practice.
 \end{warn}