changeset 25258 | 22d16596c306 |
parent 19248 | 25bb0a883ac5 |
child 35416 | d8d7d1b785af |
--- 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 \<Rightarrow> 'a"