diff -r 06206298e4d0 -r ed3964d1f1a4 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Sun Nov 26 11:37:49 2000 +0100
+++ b/doc-src/TutorialI/fp.tex	Mon Nov 27 10:38:43 2000 +0100
@@ -549,7 +549,8 @@
 defined by means of \isacommand{recdef}: you can use full pattern-matching,
 recursion need not involve datatypes, and termination is proved by showing
 that the arguments of all recursive calls are smaller in a suitable (user
-supplied) sense.
+supplied) sense. In this section we ristrict ourselves to measure functions;
+more advanced termination proofs are discussed in \S\ref{sec:beyond-measure}.
 
 \subsection{Defining recursive functions}