doc-src/TutorialI/fp.tex

 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$\\
+\item zero for all constructors that do not have an argument of type $t$,
 \item one plus the sum of the sizes of all arguments of type~$t$,
-for all other constructors
+for all other constructors.
 \end{itemize}
 Note that because
 \isa{size} is defined on every datatype, it is overloaded; on lists
 \isa{size} is also called \sdx{length}, which is not overloaded.
 Isabelle will always show \isa{size} on lists as \isa{length}.

 
 \subsection{Primitive Recursion}
 
 \index{recursion!primitive}%
 Functions on datatypes are usually defined by recursion. In fact, most of the
-time they are defined by what is called \textbf{primitive recursion}.
-The keyword \commdx{primrec} is followed by a list of
-equations
+time they are defined by what is called \textbf{primitive recursion} over some
+datatype $t$. This means that the recursion equations must be of the form
 \[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
-such that $C$ is a constructor of the datatype $t$ and all recursive calls of
+such that $C$ is a constructor of $t$ and all recursive calls of
 $f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
 Isabelle immediately sees that $f$ terminates because one (fixed!) argument
 becomes smaller with every recursive call. There must be at most one equation
 for each constructor.  Their order is immaterial.
 A more general method for defining total recursive functions is introduced in