src/Doc/Codegen/Introduction.thy
changeset 76649 9a6cb5ecc183
parent 72375 e48d93811ed7
child 76987 4c275405faae
--- 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}.