1.1 --- a/doc-src/TutorialI/fp.tex Mon Nov 05 15:04:19 2007 +0100
1.2 +++ b/doc-src/TutorialI/fp.tex Mon Nov 05 15:37:41 2007 +0100
1.3 @@ -469,8 +469,9 @@
1.4 recursion need not involve datatypes, and termination is proved by showing
1.5 that the arguments of all recursive calls are smaller in a suitable sense.
1.6 In this section we restrict ourselves to functions where Isabelle can prove
1.7 -termination automatically. User supplied termination proofs are discussed in
1.8 -{\S}\ref{sec:beyond-measure}.
1.9 +termination automatically. More advanced function definitions, including user
1.10 +supplied termination proofs, nested recursion and partiality, are discussed
1.11 +in a separate tutorial~\cite{isabelle-function}.
1.12
1.13 \input{Fun/document/fun0.tex}
1.14