summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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}