diff -r 55f33da63366 -r 458068404143 doc-src/TutorialI/Recdef/examples.thy --- 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"\(x\<^sub>1,\,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: *}