1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Wed Jun 17 10:07:23 2009 +0200
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Wed Jun 17 10:07:25 2009 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  \isa{int} of \textbf{integers}, which lack induction but support true
     1.5  subtraction.  With subtraction, arithmetic reasoning is easier, which makes
     1.6  the integers preferable to the natural numbers for
     1.7 -complicated arithmetic expressions, even if they are non-negative.  The logic HOL-Complex also has the types
     1.8 +complicated arithmetic expressions, even if they are non-negative.  There are also the types
     1.9  \isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers.  Isabelle has no 
    1.10  subtyping,  so the numeric
    1.11  types are distinct and there are functions to convert between them.
    1.12 @@ -107,7 +107,7 @@
    1.13  beginning.  Hundreds of theorems about the natural numbers are
    1.14  proved in the theories \isa{Nat} and \isa{Divides}.  
    1.15  Basic properties of addition and multiplication are available through the
    1.16 -axiomatic type class for semirings (\S\ref{sec:numeric-axclasses}).
    1.17 +axiomatic type class for semirings (\S\ref{sec:numeric-classes}).
    1.18  
    1.19  \subsubsection{Literals}
    1.20  \index{numeric literals!for type \protect\isa{nat}}%
    1.21 @@ -242,7 +242,7 @@
    1.22  proving inequalities involving integer multiplication and division, similar
    1.23  to those shown above for type~\isa{nat}. The laws of addition, subtraction
    1.24  and multiplication are available through the axiomatic type class for rings
    1.25 -(\S\ref{sec:numeric-axclasses}).
    1.26 +(\S\ref{sec:numeric-classes}).
    1.27  
    1.28  The \rmindex{absolute value} function \cdx{abs} is overloaded, and is 
    1.29  defined for all types that involve negative numbers, including the integers.
    1.30 @@ -337,8 +337,7 @@
    1.31  reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
    1.32  upper bound.  (It could only be $\surd2$, which is irrational.) The
    1.33  formalization of completeness, which is complicated, 
    1.34 -can be found in theory \texttt{RComplete} of directory
    1.35 -\texttt{Real}.
    1.36 +can be found in theory \texttt{RComplete}.
    1.37  
    1.38  Numeric literals\index{numeric literals!for type \protect\isa{real}}
    1.39  for type \isa{real} have the same syntax as those for type
    1.40 @@ -354,15 +353,13 @@
    1.41  is performed.
    1.42  
    1.43  \begin{warn}
    1.44 -Type \isa{real} is only available in the logic HOL-Complex, which is
    1.45 -HOL extended with a definitional development of the real and complex
    1.46 +Types \isa{rat}, \isa{real} and \isa{complex} are provided by theory HOL-Complex, which is
    1.47 +Main extended with a definitional development of the rational, real and complex
    1.48  numbers.  Base your theory upon theory \thydx{Complex_Main}, not the
    1.49 -usual \isa{Main}, and set the Proof General menu item \pgmenu{Isabelle} $>$
    1.50 -\pgmenu{Logics} $>$ \pgmenu{HOL-Complex}.%
    1.51 -\index{real numbers|)}\index{*real (type)|)}
    1.52 +usual \isa{Main}.%
    1.53  \end{warn}
    1.54  
    1.55 -Also available in HOL-Complex is the
    1.56 +Available in the logic HOL-NSA is the
    1.57  theory \isa{Hyperreal}, which define the type \tydx{hypreal} of 
    1.58  \rmindex{non-standard reals}.  These
    1.59  \textbf{hyperreals} include infinitesimals, which represent infinitely
    1.60 @@ -379,7 +376,7 @@
    1.61  \index{complex numbers|)}\index{*complex (type)|)}
    1.62  
    1.63  
    1.64 -\subsection{The Numeric Type Classes}\label{sec:numeric-axclasses}
    1.65 +\subsection{The Numeric Type Classes}\label{sec:numeric-classes}
    1.66  
    1.67  Isabelle/HOL organises its numeric theories using axiomatic type classes.
    1.68  Hundreds of basic properties are proved in the theory \isa{Ring_and_Field}.