doc-src/IsarAdvanced/Codegen/Thy/Program.thy

New outline for codegen tutorial -- draft

theory Program
imports Setup
begin

section {* Turning Theories into Programs *}

subsection {* The @{text "Isabelle/HOL"} default setup *}

text {* Invoking the code generator *}

subsection {* Selecting code equations *}

text {* inspection by @{text "code_thms"} *}

subsection {* The preprocessor *}

subsection {* Datatypes *}

text {* example: @{text "rat"}, cases *}

subsection {* Equality and wellsortedness *}

subsection {* Partiality *}

text {* @{text "code_abort"}, examples: maps *}

end