Using type real does not require a separate logic now.

--- a/doc-src/TutorialI/ToyList/ToyList.thy	Sun Aug 15 16:48:58 2010 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Sun Aug 15 17:14:10 2010 +0200
@@ -124,7 +124,8 @@
 
 value "rev (a # b # c # [])"
 
-text{*
+text{*\noindent yields @{term"c # b # a # []"}.
+
 \section{An Introductory Proof}
 \label{sec:intro-proof}
 

--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Sun Aug 15 16:48:58 2010 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Sun Aug 15 17:14:10 2010 +0200
@@ -147,6 +147,8 @@
 \isacommand{value}\isamarkupfalse%
 \ {\isachardoublequoteopen}rev\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ c\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
+\noindent yields \isa{c\ {\isacharhash}\ b\ {\isacharhash}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}.
+
 \section{An Introductory Proof}
 \label{sec:intro-proof}
 

--- 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}