doc-src/TutorialI/fp.tex
changeset 25281 8d309beb66d6
parent 25263 b54744935036
child 27015 f8537d69f514
     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