author paulson Thu, 08 May 2003 12:52:15 +0200 changeset 13979 4c3a638828b9 parent 13978 a241cdd9c1c9 child 13980 f254d1c92a6a
HOL-Complex
--- a/doc-src/TutorialI/Types/numerics.tex	Thu May 08 12:51:55 2003 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex	Thu May 08 12:52:15 2003 +0200
@@ -12,9 +12,10 @@
\isa{int} of \textbf{integers}, which lack induction but support true
subtraction.  The integers are preferable to the natural numbers for reasoning about
complicated arithmetic expressions, even for some expressions whose
-value is non-negative.  The logic HOL-Real also has the type
-\isa{real} of real numbers.  Isabelle has no subtyping,  so the numeric
-types are distinct and there are  functions to convert between them.
+value is non-negative.  The logic HOL-Complex also has the types
+\isa{real} and \isa{complex}: the real and complex numbers.  Isabelle has no
+subtyping,  so the numeric
+types are distinct and there are functions to convert between them.
Fortunately most numeric operations are overloaded: the same symbol can be
\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
-Induction is less important for integers than it is for the natural numbers, but it can be valuable if the range of integers has a lower or upper bound.  There are four rules for integer induction, corresponding to the possible relations of the bound ($\ge$, $>$, $\le$ and $<$):
+Induction is less important for integers than it is for the natural numbers, but it can be valuable if the range of integers has a lower or upper bound.  There are four rules for integer induction, corresponding to the possible relations of the bound ($\geq$, $>$, $\leq$ and $<$):
\rulename{int_ge_induct}\isanewline