isabelle: src/Doc/Codegen/Setup.thy@d20f19f54789 (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
46517 9d2e682a68eb tuned import haftmann parents: 43564 diff changeset	4	"~~/src/HOL/Library/Dlist"
9d2e682a68eb tuned import haftmann parents: 43564 diff changeset	5	"~~/src/HOL/Library/RBT"
9d2e682a68eb tuned import haftmann parents: 43564 diff changeset	6	"~~/src/HOL/Library/Mapping"
51162 310b94ed1815 dropped now obsolete hint; haftmann parents: 48985 diff changeset	7	"~~/src/HOL/Library/IArray"
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
48951 b9238cbcdd41 more standard document preparation within session context; wenzelm parents: 48891 diff changeset	10	(* FIXME avoid writing into source directory *)
b9238cbcdd41 more standard document preparation within session context; wenzelm parents: 48891 diff changeset	11	ML {*
56208 06cc31dff138 clarifed module name; wenzelm parents: 56061 diff changeset	12	Isabelle_System.mkdirs (Path.append (Resources.master_directory @{theory}) (Path.basic "examples"))
48951 b9238cbcdd41 more standard document preparation within session context; wenzelm parents: 48891 diff changeset	13	*}
b9238cbcdd41 more standard document preparation within session context; wenzelm parents: 48891 diff changeset	14
b9238cbcdd41 more standard document preparation within session context; wenzelm parents: 48891 diff changeset	15	ML_file "../antiquote_setup.ML"
b9238cbcdd41 more standard document preparation within session context; wenzelm parents: 48891 diff changeset	16	ML_file "../more_antiquote.ML"
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46517 diff changeset	17
38503 7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	18	setup {*
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	19	let
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	20	val typ = Simple_Syntax.read_typ;
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	21	in
56240 938c6c7e10eb tuned signature; wenzelm parents: 56239 diff changeset	22	Sign.del_syntax (Symbol.xsymbolsN, false)
42293 6cca0343ea48 renamed sprop "prop#" to "prop'" -- proper identifier; wenzelm parents: 42288 diff changeset	23	[("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
6cca0343ea48 renamed sprop "prop#" to "prop'" -- proper identifier; wenzelm parents: 42288 diff changeset	24	("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
56240 938c6c7e10eb tuned signature; wenzelm parents: 56239 diff changeset	25	Sign.add_syntax (Symbol.xsymbolsN, false)
42293 6cca0343ea48 renamed sprop "prop#" to "prop'" -- proper identifier; wenzelm parents: 42288 diff changeset	26	[("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
6cca0343ea48 renamed sprop "prop#" to "prop'" -- proper identifier; wenzelm parents: 42288 diff changeset	27	("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
38503 7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	28	end
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	29	*}
7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	30
34071 93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	31	setup {* Code_Target.set_default_code_width 74 *}
93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	32
42669 04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique; wenzelm parents: 42358 diff changeset	33	declare [[names_unique = false]]
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	34
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	35	end
46517 9d2e682a68eb tuned import haftmann parents: 43564 diff changeset	36

author	blanchet
	Fri, 16 May 2014 19:13:50 +0200
changeset 56984	d20f19f54789
parent 56240	938c6c7e10eb
child 59324	f5f9993a168d
permissions	-rw-r--r--