isabelle: src/Doc/Codegen/Setup.thy@c982a4cc8dc4 (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
59378 065f349852e6 separate image for prerequisites of codegen tutorial haftmann parents: 59377 diff changeset	4	"~~/src/Tools/Permanent_Interpretation"
46517 9d2e682a68eb tuned import haftmann parents: 43564 diff changeset	5	"~~/src/HOL/Library/Dlist"
9d2e682a68eb tuned import haftmann parents: 43564 diff changeset	6	"~~/src/HOL/Library/RBT"
9d2e682a68eb tuned import haftmann parents: 43564 diff changeset	7	"~~/src/HOL/Library/Mapping"
51162 310b94ed1815 dropped now obsolete hint; haftmann parents: 48985 diff changeset	8	"~~/src/HOL/Library/IArray"
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	9	begin
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	10
48951 b9238cbcdd41 more standard document preparation within session context; wenzelm parents: 48891 diff changeset	11	ML_file "../antiquote_setup.ML"
b9238cbcdd41 more standard document preparation within session context; wenzelm parents: 48891 diff changeset	12	ML_file "../more_antiquote.ML"
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46517 diff changeset	13
61143 5f898411ce87 eliminated \<Colon> from syntax of constraints; wenzelm parents: 59378 diff changeset	14	no_syntax (output)
5f898411ce87 eliminated \<Colon> from syntax of constraints; wenzelm parents: 59378 diff changeset	15	"_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3)
5f898411ce87 eliminated \<Colon> from syntax of constraints; wenzelm parents: 59378 diff changeset	16	"_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3)
5f898411ce87 eliminated \<Colon> from syntax of constraints; wenzelm parents: 59378 diff changeset	17
5f898411ce87 eliminated \<Colon> from syntax of constraints; wenzelm parents: 59378 diff changeset	18	syntax (output)
5f898411ce87 eliminated \<Colon> from syntax of constraints; wenzelm parents: 59378 diff changeset	19	"_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
5f898411ce87 eliminated \<Colon> from syntax of constraints; wenzelm parents: 59378 diff changeset	20	"_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3)
38503 7115853eaf8a pretty constraint syntax; tuned theory imports haftmann parents: 38460 diff changeset	21
59324 f5f9993a168d prefer option for default code printing width haftmann parents: 56240 diff changeset	22	declare [[default_code_width = 74]]
34071 93bfbb557e2e default_code_width is now proper theory data haftmann parents: 32833 diff changeset	23
42669 04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique; wenzelm parents: 42358 diff changeset	24	declare [[names_unique = false]]
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	25
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: diff changeset	26	end

author	blanchet
	Sun, 04 Oct 2015 17:41:52 +0200
changeset 61321	c982a4cc8dc4
parent 61143	5f898411ce87
child 61670	301e0b4ecd45
permissions	-rw-r--r--