--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Dec 02 14:47:07 2004 +0100
@@ -34,20 +34,20 @@
\newcommand{\mystar}{*%
}
\index{arithmetic operations!for \protect\isa{nat}}%
-The arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
-\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
+The arithmetic operations \isadxboldpos{+}{$HOL2arithfun},
+\isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun},
\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
+\isadxboldpos{\isasymle}{$HOL2arithrel} and
+\isadxboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
\isa{m\ {\isacharless}\ n}. There is even a least number operation
\sdx{LEAST}\@. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{0}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}}.
\begin{warn}\index{overloading}
The constants \cdx{0} and \cdx{1} and the operations
- \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
- \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
- \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
- \ttindexboldpos{<}{$HOL2arithrel} are overloaded: they are available
+ \isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun},
+ \isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
+ \cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and
+ \isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available
not just for natural numbers but for other types as well.
For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}, there is nothing to indicate
that you are talking about natural numbers. Hence Isabelle can only infer
@@ -65,6 +65,12 @@
overloaded operations.
\end{warn}
\begin{warn}
+ The symbols \isadxboldpos{>}{$HOL2arithrel} and
+ \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: \isa{x\ {\isachargreater}\ y}
+ stands for \isa{y\ {\isacharless}\ x} and similary for \isa{{\isasymge}} and
+ \isa{{\isasymle}}.
+\end{warn}
+\begin{warn}
Constant \isa{{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat} is defined to equal \isa{Suc\ {\isadigit{0}}}. This definition
(see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by