# HG changeset patch
# User nipkow
# Date 1281883722 -7200
# Node ID 254a021ed66e07b8c3063110f1a5cd388cad7b0c
# Parent  480b2de9927c76c8f45833bbbdb5cda650f37748
tuned text about "value" and added note on comments.

diff -r 480b2de9927c -r 254a021ed66e doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Aug 11 14:45:38 2010 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Sun Aug 15 16:48:42 2010 +0200
@@ -105,6 +105,8 @@
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
 the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
 
+Comments\index{comment} must be in enclosed in \texttt{(* }and\texttt{ *)}.
+
 \section{Evaluation}
 \index{evaluation}
 
@@ -120,17 +122,7 @@
 But we can go beyond mere functional programming and evaluate terms with
 variables in them, executing functions symbolically: *}
 
-normal_form "rev (a # b # c # [])"
-
-text{*\noindent yields @{term"c # b # a # []"}.
-Command \commdx{normal\protect\_form} works for arbitrary terms
-but can be slower than command \commdx{value},
-which is restricted to variable-free terms and executable functions.
-To appreciate the subtleties of evaluating terms with variables,
-try this one:
-*}
-
-normal_form "rev (a # b # c # xs)"
+value "rev (a # b # c # [])"
 
 text{*
 \section{An Introductory Proof}
diff -r 480b2de9927c -r 254a021ed66e doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 11 14:45:38 2010 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Sun Aug 15 16:48:42 2010 +0200
@@ -125,6 +125,8 @@
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
 the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
 
+Comments\index{comment} must be in enclosed in \texttt{(* }and\texttt{ *)}.
+
 \section{Evaluation}
 \index{evaluation}
 
@@ -142,20 +144,9 @@
 variables in them, executing functions symbolically:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{normal{\isacharunderscore}form}\isamarkupfalse%
+\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}}.
-Command \commdx{normal\protect\_form} works for arbitrary terms
-but can be slower than command \commdx{value},
-which is restricted to variable-free terms and executable functions.
-To appreciate the subtleties of evaluating terms with variables,
-try this one:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{normal{\isacharunderscore}form}\isamarkupfalse%
-\ {\isachardoublequoteopen}rev\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ c\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
 \section{An Introductory Proof}
 \label{sec:intro-proof}
 
diff -r 480b2de9927c -r 254a021ed66e doc-src/TutorialI/ToyList2/ToyList1
--- a/doc-src/TutorialI/ToyList2/ToyList1	Wed Aug 11 14:45:38 2010 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList1	Sun Aug 15 16:48:42 2010 +0200
@@ -5,6 +5,7 @@
 datatype 'a list = Nil                          ("[]")
                  | Cons 'a "'a list"            (infixr "#" 65)
 
+(* This is the append function: *)
 primrec app :: "'a list => 'a list => 'a list"  (infixr "@" 65)
 where
 "[] @ ys       = ys" |