diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Thu Nov 29 13:33:45 2001 +0100
@@ -37,8 +37,9 @@
 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.%
+\texttt{ToyList.thy}.
+% It is good practice to present all declarations and
+%definitions at the beginning of a theory to facilitate browsing.%
 \index{*ToyList example|)}
 
 \begin{figure}[htbp]
@@ -70,7 +71,7 @@
 There are two kinds of commands used during a proof: the actual proof
 commands and auxiliary commands for examining the proof state and controlling
 the display. Simple proof commands are of the form
-\commdx{apply}\isa{(\textit{method})}, where \textit{method} is typically 
+\commdx{apply}(\textit{method}), where \textit{method} is typically 
 \isa{induct_tac} or \isa{auto}.  All such theorem proving operations
 are referred to as \bfindex{methods}, and further ones are
 introduced throughout the tutorial.  Unless stated otherwise, you may
@@ -144,7 +145,8 @@
 %  theory itself. This you can do by typing
 %  \isa{\commdx{use\_thy}~"T"}.
 \end{description}
-Further commands are found in the Isabelle/Isar Reference Manual.
+Further commands are found in the Isabelle/Isar Reference
+Manual~\cite{isabelle-isar-ref}.
 
 We now examine Isabelle's functional programming constructs systematically,
 starting with inductive datatypes.
@@ -175,7 +177,7 @@
 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.
+always use HOL's predefined lists by building on theory \isa{Main}.
 
 
 \subsection{The General Format}
@@ -198,10 +200,12 @@
 during proofs by simplification.  The same is true for the equations in
 primitive recursive function definitions.
 
-Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
-the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is
-just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
-  1}.  In general, \cdx{size} returns 
+Every\footnote{Except for advanced datatypes where the recursion involves
+``\isasymRightarrow'' as in {\S}\ref{sec:nested-fun-datatype}.} datatype $t$
+comes equipped with a \isa{size} function from $t$ into the natural numbers
+(see~{\S}\ref{sec:nat} below). For lists, \isa{size} is just the length, i.e.\
+\isa{size [] = 0} and \isa{size(x \# xs) = size xs + 1}.  In general,
+\cdx{size} returns
 \begin{itemize}
 \item zero for all constructors
 that do not have an argument of type $t$\\
@@ -275,12 +279,11 @@
 
 \subsection{Type Synonyms}
 
-\index{type synonyms|(}%
+\index{type synonyms}%
 Type synonyms are similar to those found in ML\@. They are created by a 
 \commdx{types} command:
 
-\input{Misc/document/types.tex}%
-\index{type synonyms|)}
+\input{Misc/document/types.tex}
 
 \input{Misc/document/prime_def.tex}
 
@@ -397,6 +400,7 @@
 
 
 \subsection{The Limits of Nested Recursion}
+\label{sec:nested-fun-datatype}
 
 How far can we push nested recursion? By the unfolding argument above, we can
 reduce nested to mutual recursion provided the nested recursion only involves