isabelle: doc-src/Codegen/Thy/Setup.thy@2f4684e2ea95 (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",
30119 391e12ff816c fixed import of ~~/src/HOL/Decision_Procs/Ferrack; wenzelm parents: 29794 diff changeset	8	"~~/src/HOL/Decision_Procs/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

author	haftmann
	Tue, 03 Mar 2009 11:00:51 +0100
changeset 30226	2f4684e2ea95
parent 30119	doc-src/IsarAdvanced/Codegen/Thy/Setup.thy@391e12ff816c
child 30227	853abb4853cc
permissions	-rw-r--r--