author | wenzelm |
Sun, 09 Mar 2014 17:40:02 +0100 | |
changeset 56007 | 1b61dfbcf9a4 |
parent 51162 | 310b94ed1815 |
child 56059 | 2390391584c2 |
permissions | -rw-r--r-- |
28213 | 1 |
theory Setup |
39066 | 2 |
imports |
3 |
Complex_Main |
|
46517 | 4 |
"~~/src/HOL/Library/Dlist" |
5 |
"~~/src/HOL/Library/RBT" |
|
6 |
"~~/src/HOL/Library/Mapping" |
|
51162 | 7 |
"~~/src/HOL/Library/IArray" |
28213 | 8 |
begin |
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 {* |
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
48891
diff
changeset
|
12 |
Isabelle_System.mkdirs (Path.append (Thy_Load.master_directory @{theory}) (Path.basic "examples")) |
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 | 17 |
|
38503 | 18 |
setup {* |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43271
diff
changeset
|
19 |
Antiquote_Setup.setup #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43271
diff
changeset
|
20 |
More_Antiquote.setup #> |
38503 | 21 |
let |
22 |
val typ = Simple_Syntax.read_typ; |
|
23 |
in |
|
42293
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
24 |
Sign.del_modesyntax_i (Symbol.xsymbolsN, false) |
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
25 |
[("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
26 |
("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #> |
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
27 |
Sign.add_modesyntax_i (Symbol.xsymbolsN, false) |
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
28 |
[("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)), |
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
29 |
("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))] |
38503 | 30 |
end |
31 |
*} |
|
32 |
||
34071 | 33 |
setup {* Code_Target.set_default_code_width 74 *} |
34 |
||
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42358
diff
changeset
|
35 |
declare [[names_unique = false]] |
28213 | 36 |
|
37 |
end |
|
46517 | 38 |