--- a/doc-src/TutorialI/Recdef/examples.thy Wed Dec 13 09:32:55 2000 +0100
+++ b/doc-src/TutorialI/Recdef/examples.thy Wed Dec 13 09:39:53 2000 +0100
@@ -35,6 +35,8 @@
text{*\noindent
This time the measure is the length of the list, which decreases with the
recursive call; the first component of the argument tuple is irrelevant.
+The details of tupled $\lambda$-abstractions @{text"\<lambda>(x\<^sub>1,\<dots>,x\<^sub>n)"} are
+explained in \S\ref{sec:products}, but for now your intuition is all you need.
Pattern matching need not be exhaustive:
*}