doc-src/TutorialI/Advanced/Partial.thy
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"