author | wenzelm |
Sat, 16 Apr 2011 13:48:45 +0200 | |
changeset 42358 | b47d41d9f4b5 |
parent 42293 | 6cca0343ea48 |
child 42669 | 04dfffda5671 |
permissions | -rw-r--r-- |
28213 | 1 |
theory Setup |
39066 | 2 |
imports |
3 |
Complex_Main |
|
4 |
More_List RBT Dlist Mapping |
|
30227 | 5 |
uses |
6 |
"../../antiquote_setup.ML" |
|
7 |
"../../more_antiquote.ML" |
|
28213 | 8 |
begin |
9 |
||
38503 | 10 |
setup {* |
11 |
let |
|
12 |
val typ = Simple_Syntax.read_typ; |
|
13 |
in |
|
42293
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
14 |
Sign.del_modesyntax_i (Symbol.xsymbolsN, false) |
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
15 |
[("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
16 |
("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #> |
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
17 |
Sign.add_modesyntax_i (Symbol.xsymbolsN, false) |
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
18 |
[("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)), |
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
19 |
("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))] |
38503 | 20 |
end |
21 |
*} |
|
22 |
||
34071 | 23 |
setup {* Code_Target.set_default_code_width 74 *} |
24 |
||
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42293
diff
changeset
|
25 |
declare [[unique_names = false]] |
28213 | 26 |
|
27 |
end |