diff -r 7917e66505a4 -r 6852682eaf16 doc-src/TutorialI/Misc/document/natsum.tex
--- 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,%