--- a/doc-src/TutorialI/ToyList/ToyList.thy Sun Aug 15 13:17:45 2010 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Sun Aug 15 16:48:58 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}
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Sun Aug 15 13:17:45 2010 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Sun Aug 15 16:48:58 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}
--- a/doc-src/TutorialI/ToyList2/ToyList1 Sun Aug 15 13:17:45 2010 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList1 Sun Aug 15 16:48:58 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" |