doc-src/TutorialI/basics.tex

 \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual}
 for more details.}.
 
 \begin{pgnote}
 You can choose a different logic via the \pgmenu{Isabelle} $>$
-\pgmenu{Logics} menu. For example, you may want to work in the real
-numbers, an extension of HOL (see \S\ref{sec:real}).
+\pgmenu{Logics} menu.
 \end{pgnote}