isabelle: doc-src/Codegen/Thy/Setup.thy@3bc28ce6986c (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
43271 8b968645d216 updated imports (cf. 93b1183e43e5); wenzelm parents: 42669 diff changeset	4	More_List RBT Dlist List_Cset 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	in
42293 6cca0343ea48 renamed sprop "prop#" to "prop'" -- proper identifier; wenzelm parents: 42288 diff changeset	14	Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
6cca0343ea48 renamed sprop "prop#" to "prop'" -- proper identifier; wenzelm parents: 42288 diff changeset	15	[("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
6cca0343ea48 renamed sprop "prop#" to "prop'" -- proper identifier; wenzelm parents: 42288 diff changeset	16	("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
6cca0343ea48 renamed sprop "prop#" to "prop'" -- proper identifier; wenzelm parents: 42288 diff changeset	17	Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
6cca0343ea48 renamed sprop "prop#" to "prop'" -- proper identifier; wenzelm parents: 42288 diff changeset	18	[("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
6cca0343ea48 renamed sprop "prop#" to "prop'" -- proper identifier; wenzelm parents: 42288 diff changeset	19	("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
38503 7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	20	end
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	21	*}
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	22
34071 93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	23	setup {* Code_Target.set_default_code_width 74 *}
93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	24
42669 04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique; wenzelm parents: 42358 diff changeset	25	declare [[names_unique = false]]
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	26
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	27	end

author	bulwahn
	Thu, 09 Jun 2011 08:32:14 +0200
changeset 43309	3bc28ce6986c
parent 43271	8b968645d216
child 43564	9864182c6bad
permissions	-rw-r--r--