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}