isabelle: doc-src/Codegen/Thy/Setup.thy@628fee3eb449 (annotated)

28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	1	theory Setup
38460 628fee3eb449 nicer code for rev haftmann parents: 34071 diff changeset	2	imports Complex_Main More_List
30227 853abb4853cc tuned manuals haftmann parents: 30226 diff changeset	3	uses
853abb4853cc tuned manuals haftmann parents: 30226 diff changeset	4	"../../antiquote_setup.ML"
853abb4853cc tuned manuals haftmann parents: 30226 diff changeset	5	"../../more_antiquote.ML"
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	6	begin
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	7
28447 df77ed974a78 fixed haftmann parents: 28440 diff changeset	8	ML {* no_document use_thys
29514 fc20414d4aa8 fixed location of Imperative_HOL haftmann parents: 29295 diff changeset	9	["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	10	"~~/src/HOL/Decision_Procs/Ferrack"] *}
28419 f65e8b318581 re-canibalised manual haftmann parents: 28213 diff changeset	11
34071 93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	12	setup {* Code_Target.set_default_code_width 74 *}
93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	13
32833 f3716d1a2e48 explicitly Unsynchronized; wenzelm parents: 30227 diff changeset	14	ML_command {* Unsynchronized.reset unique_names *}
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	15
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	16	end

author	haftmann
	Tue, 17 Aug 2010 14:19:12 +0200
changeset 38460	628fee3eb449
parent 34071	93bfbb557e2e
child 38503	7115853eaf8a
permissions	-rw-r--r--