
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 \<Rightarrow> 'a"




