--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Jan 10 01:13:41 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Jan 10 11:22:03 2002 +0100
@@ -128,7 +128,7 @@
Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
role, it may fail to prove a valid formula, for example
- \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}}. Fortunately, such examples are rare.
+ \isa{m{\isacharplus}m\ {\isasymnoteq}\ n{\isacharplus}n{\isacharplus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. Fortunately, such examples are rare.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%