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

+
+(* $Id$ *)
+
+theory Codegen
+imports Main
+begin
+
+chapter {* Code generation from Isabelle theories *}
+
+section {* Introduction *}
+
+text {*
+  \cite{isa-tutorial}
+*} (* add graphics here *)
+
+section {* Basics *}
+
+subsection {* Invoking the code generator *}
+
+subsection {* Theorem selection *}
+
+(* print_codethms, code func, default setup code nofunc *)
+
+subsection {* Type classes *}
+
+subsection {* Preprocessing *}
+
+(* preprocessing, print_codethms () *)
+
+subsection {* Incremental code generation *}
+
+(* print_codethms (\<dots>) *)
+
+
+section {* Customizing serialization  *}
+
+section {* Recipes and advanced topics *}
+
+(* understanding the type game, reflexive equations, code inline code_constsubst, code_abstype*)
+
+section {* ML interfaces *}
+
+subsection {* codegen\_data.ML *}
+
+subsection {* Implementing code generator applications *}
+
+end