diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/Advanced/Partial.thy --- a/doc-src/TutorialI/Advanced/Partial.thy Thu Nov 01 13:44:44 2007 +0100 +++ b/doc-src/TutorialI/Advanced/Partial.thy Thu Nov 01 20:20:19 2007 +0100 @@ -22,7 +22,7 @@ We have already seen an instance of underdefinedness by means of non-exhaustive pattern matching: the definition of @{term last} in -\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec} +\S\ref{sec:fun}. The same is allowed for \isacommand{primrec} *} consts hd :: "'a list \ 'a"