isabelle: doc-src/Codegen/Thy/Setup.thy@8f37cf60b885 (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
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
30227 853abb4853cc tuned manuals haftmann parents: 30226 diff changeset	12	ML_command {* Code_Target.code_width := 74 *}
853abb4853cc tuned manuals haftmann parents: 30226 diff changeset	13	ML_command {* reset unique_names *}
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	14
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	15	end

author	nipkow
	Sun, 12 Jul 2009 14:48:01 +0200
changeset 31995	8f37cf60b885
parent 30227	853abb4853cc
child 32833	f3716d1a2e48
permissions	-rw-r--r--