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