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}.