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

28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	1	theory Setup
39066 4517a4049588 more canonical theory setup haftmann parents: 38798 diff changeset	2	imports
4517a4049588 more canonical theory setup haftmann parents: 38798 diff changeset	3	Complex_Main
4517a4049588 more canonical theory setup haftmann parents: 38798 diff changeset	4	More_List RBT Dlist Mapping
30227 853abb4853cc tuned manuals haftmann parents: 30226 diff changeset	5	uses
853abb4853cc tuned manuals haftmann parents: 30226 diff changeset	6	"../../antiquote_setup.ML"
853abb4853cc tuned manuals haftmann parents: 30226 diff changeset	7	"../../more_antiquote.ML"
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	8	begin
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	9
38503 7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	10	setup {*
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	11	let
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	12	val typ = Simple_Syntax.read_typ;
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	13	val typeT = Syntax.typeT;
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	14	val spropT = Syntax.spropT;
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	15	in
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	16	Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	17	("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	18	("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	19	#> Sign.add_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	end
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	23	*}
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	24
34071 93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	25	setup {* Code_Target.set_default_code_width 74 *}
93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	26
38798 89f273ab1d42 expanded some aliases from structure Unsynchronized; wenzelm parents: 38503 diff changeset	27	ML_command {* unique_names := false *}
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	28
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	29	end

author	blanchet
	Mon, 21 Feb 2011 14:02:07 +0100
changeset 41800	7f333b59d5fb
parent 39066	4517a4049588
child 42288	2074b31650e6
permissions	-rw-r--r--