doc-src/TutorialI/fp.tex
 changeset 10654 458068404143 parent 10608 620647438780 child 10795 9e888d60d3e5
     1.1 --- a/doc-src/TutorialI/fp.tex	Wed Dec 13 09:32:55 2000 +0100
1.2 +++ b/doc-src/TutorialI/fp.tex	Wed Dec 13 09:39:53 2000 +0100
1.3 @@ -206,7 +206,7 @@
1.4  such that $C$ is a constructor of the datatype $t$ and all recursive calls of
1.5  $f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
1.6  Isabelle immediately sees that $f$ terminates because one (fixed!) argument
1.7 -becomes smaller with every recursive call. There must be exactly one equation
1.8 +becomes smaller with every recursive call. There must be at most one equation
1.9  for each constructor.  Their order is immaterial.
1.10  A more general method for defining total recursive functions is introduced in
1.11  {\S}\ref{sec:recdef}.
1.12 @@ -472,7 +472,7 @@
1.13  more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
1.14
1.15  \subsection{Defining recursive functions}
1.16 -
1.17 +\label{sec:recdef-examples}
1.18  \input{Recdef/document/examples.tex}
1.19
1.20  \subsection{Proving termination}