--- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Tue Jul 17 13:46:21 2001 +0200
@@ -26,13 +26,13 @@
}
The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
-\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
-\isaindexbold{max} are predefined, as are the relations
+\sdx{div}, \sdx{mod}, \cdx{min} and
+\cdx{max} are predefined, as are the relations
\indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
\isa{m\ {\isacharless}\ n}. There is even a least number operation
-\isaindexbold{LEAST}. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
-Isabelle does not prove this completely automatically. Note that \isa{{\isadigit{1}}}
+\sdx{LEAST}\@. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
+Isabelle does not prove this automatically. Note that \isa{{\isadigit{1}}}
and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
\isa{Suc}-expressions. If you need the full set of numerals,
see~\S\ref{sec:numerals}.
@@ -40,8 +40,8 @@
\begin{warn}
The constant \cdx{0} and the operations
\ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
- \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
- \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
+ \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
+ \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
not just for natural numbers but at other types as well.
For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
@@ -76,7 +76,7 @@
\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.
+known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
For example,%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
@@ -93,8 +93,8 @@
\begin{warn}
The running time of \isa{arith} is exponential in the number of occurrences
- of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
- \isaindexbold{max} because they are first eliminated by case distinctions.
+ of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
+ \cdx{max} because they are first eliminated by case distinctions.
\isa{arith} is incomplete even for the restricted class of
linear arithmetic formulae. If divisibility plays a