now refers to Complex and Complex_Main
authorpaulson
Thu May 08 15:23:21 2003 +0200 (2003-05-08)
changeset 13983afc0dadddaa4
parent 13982 8abae6b7084c
child 13984 e055ba9020eb
now refers to Complex and Complex_Main
doc-src/TutorialI/Types/numerics.tex
     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