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

28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	1	theory Setup
38503 7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	2	imports Complex_Main More_List RBT Dlist Mapping
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
38503 7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	9	["Efficient_Nat", "Code_Char_chr", "Product_ord",
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	10	"~~/src/HOL/Imperative_HOL/Imperative_HOL",
30119 391e12ff816c fixed import of ~~/src/HOL/Decision_Procs/Ferrack; wenzelm parents: 29794 diff changeset	11	"~~/src/HOL/Decision_Procs/Ferrack"] *}
28419 f65e8b318581 re-canibalised manual haftmann parents: 28213 diff changeset	12
38503 7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	13	setup {*
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	14	let
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	15	val typ = Simple_Syntax.read_typ;
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	16	val typeT = Syntax.typeT;
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	17	val spropT = Syntax.spropT;
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	18	in
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	19	Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	20	("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	21	("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	22	#> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	23	("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	24	("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	25	end
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	26	*}
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	27
34071 93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	28	setup {* Code_Target.set_default_code_width 74 *}
93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	29
32833 f3716d1a2e48 explicitly Unsynchronized; wenzelm parents: 30227 diff changeset	30	ML_command {* Unsynchronized.reset unique_names *}
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	31
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	32	end

author	blanchet
	Wed, 25 Aug 2010 09:05:22 +0200
changeset 38740	e2d58749194b
parent 38503	7115853eaf8a
child 38798	89f273ab1d42
permissions	-rw-r--r--