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