diff -r f8826fc8c419 -r 9a6cb5ecc183 src/Doc/Functions/Functions.thy
--- a/src/Doc/Functions/Functions.thy	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/Functions/Functions.thy	Fri Dec 16 18:11:03 2022 +0100
@@ -750,7 +750,7 @@
 termination by (relation "{}") simp
 
 
-section \<open>Partiality\<close>
+section \<open>Partiality \label{sec:partiality}\<close>
 
 text \<open>
   In HOL, all functions are total. A function \<^term>\<open>f\<close> applied to