|
haftmann@28213
|
1 |
theory Setup
|
|
haftmann@38503
|
2 |
imports Complex_Main More_List RBT Dlist Mapping
|
|
haftmann@30227
|
3 |
uses
|
|
haftmann@30227
|
4 |
"../../antiquote_setup.ML"
|
|
haftmann@30227
|
5 |
"../../more_antiquote.ML"
|
|
haftmann@28213
|
6 |
begin
|
|
haftmann@28213
|
7 |
|
|
haftmann@28447
|
8 |
ML {* no_document use_thys
|
|
haftmann@38503
|
9 |
["Efficient_Nat", "Code_Char_chr", "Product_ord",
|
|
haftmann@38503
|
10 |
"~~/src/HOL/Imperative_HOL/Imperative_HOL",
|
|
wenzelm@30119
|
11 |
"~~/src/HOL/Decision_Procs/Ferrack"] *}
|
|
haftmann@28419
|
12 |
|
|
haftmann@38503
|
13 |
setup {*
|
|
haftmann@38503
|
14 |
let
|
|
haftmann@38503
|
15 |
val typ = Simple_Syntax.read_typ;
|
|
haftmann@38503
|
16 |
val typeT = Syntax.typeT;
|
|
haftmann@38503
|
17 |
val spropT = Syntax.spropT;
|
|
haftmann@38503
|
18 |
in
|
|
haftmann@38503
|
19 |
Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
|
|
haftmann@38503
|
20 |
("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
|
|
haftmann@38503
|
21 |
("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
|
|
haftmann@38503
|
22 |
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
|
|
haftmann@38503
|
23 |
("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
|
|
haftmann@38503
|
24 |
("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
|
|
haftmann@38503
|
25 |
end
|
|
haftmann@38503
|
26 |
*}
|
|
haftmann@38503
|
27 |
|
|
haftmann@34071
|
28 |
setup {* Code_Target.set_default_code_width 74 *}
|
|
haftmann@34071
|
29 |
|
|
wenzelm@32833
|
30 |
ML_command {* Unsynchronized.reset unique_names *}
|
|
haftmann@28213
|
31 |
|
|
haftmann@28213
|
32 |
end
|