isabelle: doc-src/IsarAdvanced/Codegen/Thy/Setup.thy@f3043dafef5f (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
29514 fc20414d4aa8 fixed location of Imperative_HOL haftmann parents: 29295 diff changeset	7	["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL",
29794 32d00a2a6f28 added stub about datatype abstraction haftmann parents: 29514 diff changeset	8	"~~/src/HOL/Reflection/Ferrack"] *}
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