# HG changeset patch
# User paulson
# Date 1052391135 -7200
# Node ID 4c3a638828b97a51ec30e70b39a8f7194950df9b
# Parent  a241cdd9c1c94984b121f8054cc2872656301d19
HOL-Complex

diff -r a241cdd9c1c9 -r 4c3a638828b9 doc-src/TutorialI/Types/numerics.tex
--- 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
 used at all numeric types. Table~\ref{tab:overloading} in the appendix
 shows the most important operations, together with the priorities of the
@@ -363,7 +364,7 @@
 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
 \index{integers|)}\index{*int (type)|)}
 
-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 $<$):
 \begin{isabelle}
 \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
 \rulename{int_ge_induct}\isanewline