author paulson Thu May 08 15:23:21 2003 +0200 (2003-05-08) changeset 13983 afc0dadddaa4 parent 13982 8abae6b7084c child 13984 e055ba9020eb
now refers to Complex and Complex_Main
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Thu May 08 13:37:51 2003 +0200
1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Thu May 08 15:23:21 2003 +0200
1.3 @@ -457,19 +457,19 @@
1.4
1.5
1.6  \begin{warn}
1.7 -Type \isa{real} is only available in the logic HOL-Real, which
1.8 -is  HOL extended with a definitional development of the real
1.9 +Type \isa{real} is only available in the logic HOL-Complex, which
1.10 +is  HOL extended with a definitional development of the real and complex
1.11  numbers.  Base your theory upon theory
1.12 -\thydx{Real}, not the usual \isa{Main}.%
1.13 +\thydx{Complex_Main}, not the usual \isa{Main}.%
1.14  \index{real numbers|)}\index{*real (type)|)}
1.15  Launch Isabelle using the command
1.16  \begin{verbatim}
1.17 -Isabelle -l HOL-Real
1.18 +Isabelle -l HOL-Complex
1.19  \end{verbatim}
1.20  \end{warn}
1.21
1.22 -Also distributed with Isabelle is HOL-Hyperreal,
1.23 -whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of
1.24 +Also available in HOL-Complex is the
1.25 +theory \isa{Hyperreal}, which define the type \tydx{hypreal} of
1.26  \rmindex{non-standard reals}.  These
1.27  \textbf{hyperreals} include infinitesimals, which represent infinitely
1.28  small and infinitely large quantities; they facilitate proofs