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