
diff -r f8826fc8c419 -r 9a6cb5ecc183 src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/Codegen/Introduction.thy	Fri Dec 16 18:11:03 2022 +0100
@@ -222,6 +222,9 @@
       dramatically by applying refinement techniques, which are
       introduced in \secref{sec:refinement}.
 
+    \item How to define partial functions such that code can be generated
+      is explained in \secref{sec:partial}.
+
     \item Inductive predicates can be turned executable using an
       extension of the code generator \secref{sec:inductive}.
 




