1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Fri Jun 10 17:59:12 2005 +0200
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Fri Jun 10 18:36:47 2005 +0200
     1.3 @@ -309,6 +309,7 @@
     1.4  
     1.5  
     1.6  \subsection{The Types of Rational, Real and Complex Numbers}
     1.7 +\label{sec:real}
     1.8  
     1.9  \index{rational numbers|(}\index{*rat (type)|(}%
    1.10  \index{real numbers|(}\index{*real (type)|(}%
    1.11 @@ -340,15 +341,12 @@
    1.12  is performed.
    1.13  
    1.14  \begin{warn}
    1.15 -Type \isa{real} is only available in the logic HOL-Complex, which
    1.16 -is  HOL extended with a definitional development of the real and complex
    1.17 -numbers.  Base your theory upon theory
    1.18 -\thydx{Complex_Main}, not the usual \isa{Main}.%
    1.19 +Type \isa{real} is only available in the logic HOL-Complex, which is
    1.20 +HOL extended with a definitional development of the real and complex
    1.21 +numbers.  Base your theory upon theory \thydx{Complex_Main}, not the
    1.22 +usual \isa{Main}, and set the Proof General menu item \textsf{Isabelle} $>$
    1.23 +\textsf{Logics} $>$ \textsf{HOL-Complex}.%
    1.24  \index{real numbers|)}\index{*real (type)|)}
    1.25 -Launch Isabelle using the command 
    1.26 -\begin{verbatim}
    1.27 -Isabelle -l HOL-Complex
    1.28 -\end{verbatim}
    1.29  \end{warn}
    1.30  
    1.31  Also available in HOL-Complex is the