# HG changeset patch
# User nipkow
# Date 1281885250 -7200
# Node ID 439f50a241c17fbb6066facf08eb3961c6a4035b
# Parent  c14a465266978ba7255aafbfd7ac3ae8237f353b
Using type real does not require a separate logic now.

diff -r c14a46526697 -r 439f50a241c1 doc-src/TutorialI/ToyList/ToyList.thy
--- 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}
 
diff -r c14a46526697 -r 439f50a241c1 doc-src/TutorialI/ToyList/document/ToyList.tex
--- 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}
 
diff -r c14a46526697 -r 439f50a241c1 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}