# HG changeset patch
# User paulson
# Date 1052400201 -7200
# Node ID afc0dadddaa498c224819b0f0e47aee9f9500eb9
# Parent  8abae6b7084c11b4f01689a34db5e03fd451995d
now refers to Complex and Complex_Main

diff -r 8abae6b7084c -r afc0dadddaa4 doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Thu May 08 13:37:51 2003 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex	Thu May 08 15:23:21 2003 +0200
@@ -457,19 +457,19 @@
 
 
 \begin{warn}
-Type \isa{real} is only available in the logic HOL-Real, which
-is  HOL extended with a definitional development of the real
+Type \isa{real} is only available in the logic HOL-Complex, which
+is  HOL extended with a definitional development of the real and complex
 numbers.  Base your theory upon theory
-\thydx{Real}, not the usual \isa{Main}.%
+\thydx{Complex_Main}, not the usual \isa{Main}.%
 \index{real numbers|)}\index{*real (type)|)}
 Launch Isabelle using the command 
 \begin{verbatim}
-Isabelle -l HOL-Real
+Isabelle -l HOL-Complex
 \end{verbatim}
 \end{warn}
 
-Also distributed with Isabelle is HOL-Hyperreal,
-whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of 
+Also available in HOL-Complex is the
+theory \isa{Hyperreal}, which define the type \tydx{hypreal} of 
 \rmindex{non-standard reals}.  These
 \textbf{hyperreals} include infinitesimals, which represent infinitely
 small and infinitely large quantities; they facilitate proofs