summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/TutorialI/Types/numerics.tex

changeset 10978 | 5eebea8f359f |

parent 10881 | 03f06372230b |

child 10983 | 59961d32b1ae |

1.1 --- a/doc-src/TutorialI/Types/numerics.tex Thu Jan 25 11:59:52 2001 +0100 1.2 +++ b/doc-src/TutorialI/Types/numerics.tex Thu Jan 25 15:31:31 2001 +0100 1.3 @@ -6,7 +6,10 @@ 1.4 \isa{int} of \textbf{integers}, which lack induction but support true 1.5 subtraction. The logic HOL-Real also has the type \isa{real} of real 1.6 numbers. Isabelle has no subtyping, so the numeric types are distinct and 1.7 -there are functions to convert between them. 1.8 +there are functions to convert between them. Fortunately most numeric 1.9 +operations are overloaded: the same symbol can be used at all numeric types. 1.10 +Table~\ref{tab:overloading} in the appendix shows the most important operations, 1.11 +together with the priorities of the infix symbols. 1.12 1.13 The integers are preferable to the natural numbers for reasoning about 1.14 complicated arithmetic expressions. For example, a termination proof