doc-src/TutorialI/basics.tex

--- a/doc-src/TutorialI/basics.tex	Sun Aug 15 16:48:58 2010 +0200
+++ b/doc-src/TutorialI/basics.tex	Sun Aug 15 17:14:10 2010 +0200
@@ -346,6 +346,5 @@
 
 \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}