src/Doc/Codegen/Introduction.thy

 
     \item The scope and quality of generated code can be increased
       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}.
 
     \item If you want to utilize code generation to obtain fast
       evaluators e.g.~for decision procedures, have a look at