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