--- a/doc-src/TutorialI/Misc/document/natsum.tex Fri Jul 13 17:56:05 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Fri Jul 13 17:58:39 2001 +0200
@@ -38,7 +38,7 @@
see~\S\ref{sec:numerals}.
\begin{warn}
- The constant \ttindexbold{0} and the operations
+ The constant \cdx{0} and the operations
\ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
\ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
\isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
@@ -70,7 +70,7 @@
is proved automatically. The main restriction is that only addition is taken
into account; other arithmetic operations and quantified formulae are ignored.
-For more complex goals, there is the special method \isaindexbold{arith}
+For more complex goals, there is the special method \methdx{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{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},