isabelle: doc-src/IsarAdvanced/Codegen/Thy/Setup.thy@f831192b9366 (annotated)

28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	1	theory Setup
28419 f65e8b318581 re-canibalised manual haftmann parents: 28213 diff changeset	2	imports Complex_Main
28440 0b9ddfa6458e added more_antiquote.ML haftmann parents: 28428 diff changeset	3	uses "../../../antiquote_setup.ML" "../../../more_antiquote.ML"
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	4	begin
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	5
28447 df77ed974a78 fixed haftmann parents: 28440 diff changeset	6	ML {* no_document use_thys
28593 f087237af65d continued codegen tutorial haftmann parents: 28447 diff changeset	7	["Efficient_Nat", "Code_Char_chr", "Product_ord", "Imperative_HOL",
29295 93b819a44146 proper import of ~~/src/HOL/ex/ReflectedFerrack; wenzelm parents: 28593 diff changeset	8	"~~/src/HOL/ex/ReflectedFerrack"] *}
28419 f65e8b318581 re-canibalised manual haftmann parents: 28213 diff changeset	9
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	10	ML_val {* Code_Target.code_width := 74 *}
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	11
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	12	end