--- a/doc-src/TutorialI/fp.tex Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Fri Jan 05 18:32:57 2001 +0100
@@ -29,8 +29,8 @@
{\makeatother\input{ToyList/document/ToyList.tex}}
-The complete proof script is shown in figure~\ref{fig:ToyList-proofs}. The
-concatenation of figures \ref{fig:ToyList} and \ref{fig:ToyList-proofs}
+The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
+concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
constitutes the complete theory \texttt{ToyList} and should reside in file
\texttt{ToyList.thy}. It is good practice to present all declarations and
definitions at the beginning of a theory to facilitate browsing.
@@ -159,7 +159,10 @@
The latter contains many further operations. For example, the functions
\isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first
element and the remainder of a list. (However, pattern-matching is usually
-preferable to \isa{hd} and \isa{tl}.) Theory \isa{List} also contains
+preferable to \isa{hd} and \isa{tl}.)
+Also available are the higher-order
+functions \isa{map}, \isa{filter}, \isa{foldl} and \isa{foldr}.
+Theory \isa{List} also contains
more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
$x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we
always use HOL's predefined lists.
@@ -193,7 +196,7 @@
\isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because
\isa{size} is defined on every datatype, it is overloaded; on lists
\isa{size} is also called \isaindexbold{length}, which is not overloaded.
-Isbelle will always show \isa{size} on lists as \isa{length}.
+Isabelle will always show \isa{size} on lists as \isa{length}.
\subsection{Primitive recursion}
@@ -261,7 +264,7 @@
\subsection{Type synonyms}
\indexbold{type synonym}
-Type synonyms are similar to those found in ML. Their syntax is fairly self
+Type synonyms are similar to those found in ML\@. Their syntax is fairly self
explanatory:
\input{Misc/document/types.tex}%
@@ -294,7 +297,7 @@
\label{sec:Simplification}
\index{simplification|(}
-So far we have proved our theorems by \isa{auto}, which ``simplifies''
+So far we have proved our theorems by \isa{auto}, which simplifies
\emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
that it did not need to so far. However, when you go beyond toy examples, you
need to understand the ingredients of \isa{auto}. This section covers the
@@ -363,7 +366,8 @@
\begin{isabelle}
\isacommand{datatype} t = C "t \isasymRightarrow\ bool"
\end{isabelle}
-is a real can of worms: in HOL it must be ruled out because it requires a type
+This declaration is a real can of worms.
+In HOL it must be ruled out because it requires a type
\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
same cardinality---an impossibility. For the same reason it is not possible
to allow recursion involving the type \isa{set}, which is isomorphic to
@@ -384,8 +388,10 @@
\begin{isabelle}
\isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
\end{isabelle}
-do indeed make sense (but note the intentionally different arrow
-\isa{\isasymrightarrow}). There is even a version of LCF on top of HOL,
+do indeed make sense. Note the different arrow,
+\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
+expressing the type of \textbf{continuous} functions.
+There is even a version of LCF on top of HOL,
called HOLCF~\cite{MuellerNvOS99}.
\index{*primrec|)}