1.1 --- a/doc-src/TutorialI/fp.tex	Fri Jan 05 18:32:33 2001 +0100
     1.2 +++ b/doc-src/TutorialI/fp.tex	Fri Jan 05 18:32:57 2001 +0100
     1.3 @@ -29,8 +29,8 @@
     1.4  
     1.5  {\makeatother\input{ToyList/document/ToyList.tex}}
     1.6  
     1.7 -The complete proof script is shown in figure~\ref{fig:ToyList-proofs}. The
     1.8 -concatenation of figures \ref{fig:ToyList} and \ref{fig:ToyList-proofs}
     1.9 +The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
    1.10 +concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
    1.11  constitutes the complete theory \texttt{ToyList} and should reside in file
    1.12  \texttt{ToyList.thy}. It is good practice to present all declarations and
    1.13  definitions at the beginning of a theory to facilitate browsing.
    1.14 @@ -159,7 +159,10 @@
    1.15  The latter contains many further operations. For example, the functions
    1.16  \isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first
    1.17  element and the remainder of a list. (However, pattern-matching is usually
    1.18 -preferable to \isa{hd} and \isa{tl}.)  Theory \isa{List} also contains
    1.19 +preferable to \isa{hd} and \isa{tl}.)  
    1.20 +Also available are the higher-order
    1.21 +functions \isa{map}, \isa{filter}, \isa{foldl} and \isa{foldr}.
    1.22 +Theory \isa{List} also contains
    1.23  more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
    1.24  $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
    1.25  always use HOL's predefined lists.
    1.26 @@ -193,7 +196,7 @@
    1.27  \isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because
    1.28  \isa{size} is defined on every datatype, it is overloaded; on lists
    1.29  \isa{size} is also called \isaindexbold{length}, which is not overloaded.
    1.30 -Isbelle will always show \isa{size} on lists as \isa{length}.
    1.31 +Isabelle will always show \isa{size} on lists as \isa{length}.
    1.32  
    1.33  
    1.34  \subsection{Primitive recursion}
    1.35 @@ -261,7 +264,7 @@
    1.36  \subsection{Type synonyms}
    1.37  \indexbold{type synonym}
    1.38  
    1.39 -Type synonyms are similar to those found in ML. Their syntax is fairly self
    1.40 +Type synonyms are similar to those found in ML\@. Their syntax is fairly self
    1.41  explanatory:
    1.42  
    1.43  \input{Misc/document/types.tex}%
    1.44 @@ -294,7 +297,7 @@
    1.45  \label{sec:Simplification}
    1.46  \index{simplification|(}
    1.47  
    1.48 -So far we have proved our theorems by \isa{auto}, which ``simplifies''
    1.49 +So far we have proved our theorems by \isa{auto}, which simplifies
    1.50  \emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
    1.51  that it did not need to so far. However, when you go beyond toy examples, you
    1.52  need to understand the ingredients of \isa{auto}.  This section covers the
    1.53 @@ -363,7 +366,8 @@
    1.54  \begin{isabelle}
    1.55  \isacommand{datatype} t = C "t \isasymRightarrow\ bool"
    1.56  \end{isabelle}
    1.57 -is a real can of worms: in HOL it must be ruled out because it requires a type
    1.58 +This declaration is a real can of worms.
    1.59 +In HOL it must be ruled out because it requires a type
    1.60  \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
    1.61  same cardinality---an impossibility. For the same reason it is not possible
    1.62  to allow recursion involving the type \isa{set}, which is isomorphic to
    1.63 @@ -384,8 +388,10 @@
    1.64  \begin{isabelle}
    1.65  \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
    1.66  \end{isabelle}
    1.67 -do indeed make sense (but note the intentionally different arrow
    1.68 -\isa{\isasymrightarrow}). There is even a version of LCF on top of HOL,
    1.69 +do indeed make sense.  Note the different arrow,
    1.70 +\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
    1.71 +expressing the type of \textbf{continuous} functions. 
    1.72 +There is even a version of LCF on top of HOL,
    1.73  called HOLCF~\cite{MuellerNvOS99}.
    1.74  
    1.75  \index{*primrec|)}