1 theory Setup |
|
2 imports |
|
3 Complex_Main |
|
4 "~~/src/HOL/Library/Dlist" |
|
5 "~~/src/HOL/Library/RBT" |
|
6 "~~/src/HOL/Library/Mapping" |
|
7 begin |
|
8 |
|
9 (* FIXME avoid writing into source directory *) |
|
10 ML {* |
|
11 Isabelle_System.mkdirs (Path.append (Thy_Load.master_directory @{theory}) (Path.basic "examples")) |
|
12 *} |
|
13 |
|
14 ML_file "../antiquote_setup.ML" |
|
15 ML_file "../more_antiquote.ML" |
|
16 |
|
17 setup {* |
|
18 Antiquote_Setup.setup #> |
|
19 More_Antiquote.setup #> |
|
20 let |
|
21 val typ = Simple_Syntax.read_typ; |
|
22 in |
|
23 Sign.del_modesyntax_i (Symbol.xsymbolsN, false) |
|
24 [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
|
25 ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #> |
|
26 Sign.add_modesyntax_i (Symbol.xsymbolsN, false) |
|
27 [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)), |
|
28 ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))] |
|
29 end |
|
30 *} |
|
31 |
|
32 setup {* Code_Target.set_default_code_width 74 *} |
|
33 |
|
34 declare [[names_unique = false]] |
|
35 |
|
36 end |
|
37 |
|