--- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Jan 24 12:29:10 2001 +0100
@@ -69,7 +69,8 @@
For more complex goals, there is the special method \isaindexbold{arith}
(which attacks the first subgoal). It proves arithmetic goals involving the
usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
-\isa{{\isasymlongrightarrow}}), the relations \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations
+\isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
+and the operations
\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
For example,%