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