added syntax for _idtdummy, _idtypdummy;
authorwenzelm
Fri Oct 07 22:59:25 2005 +0200 (2005-10-07)
changeset 17787b6e0d8323c0e
parent 17786 f06d6498ebf0
child 17788 86c46583670f
added syntax for _idtdummy, _idtypdummy;
removed obsolete _K;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Oct 07 22:59:24 2005 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Oct 07 22:59:25 2005 +0200
     1.3 @@ -219,7 +219,9 @@
     1.4    ("",            "'a => " ^ SynExt.args,      Delimfix "_"),
     1.5    ("_args",       "['a, " ^ SynExt.args ^ "] => " ^ SynExt.args, Delimfix "_,/ _"),
     1.6    ("",            "id => idt",                 Delimfix "_"),
     1.7 +  ("_idtdummy",   "idt",                       Delimfix "'_"),
     1.8    ("_idtyp",      "[id, type] => idt",         Mixfix ("_::_", [], 0)),
     1.9 +  ("_idtypdummy", "type => idt",               Mixfix ("'_()::_", [], 0)),
    1.10    ("",            "idt => idt",                Delimfix "'(_')"),
    1.11    ("",            "idt => idts",               Delimfix "_"),
    1.12    ("_idts",       "[idt, idts] => idts",       Mixfix ("_/ _", [1, 0], 0)),
    1.13 @@ -237,7 +239,6 @@
    1.14    ("_ofclass",    "[type, logic] => prop",     Delimfix "(1OFCLASS/(1'(_,/ _')))"),
    1.15    ("_mk_ofclass", "_",                         NoSyn),
    1.16    ("_TYPE",       "type => logic",             Delimfix "(1TYPE/(1'(_')))"),
    1.17 -  ("_K",          "_",                         NoSyn),
    1.18    ("",            "id => logic",               Delimfix "_"),
    1.19    ("",            "longid => logic",           Delimfix "_"),
    1.20    ("",            "var => logic",              Delimfix "_"),
    1.21 @@ -269,6 +270,7 @@
    1.22    ("_ofsort",  "[tid, sort] => type",   Mixfix ("_\\<Colon>_", [SynExt.max_pri, 0], SynExt.max_pri)),
    1.23    ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
    1.24    ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
    1.25 +  ("_idtypdummy", "type => idt",        Mixfix ("'_()\\<Colon>_", [], 0)),
    1.26    ("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    1.27    ("==",       "['a, 'a] => prop",      InfixrName ("\\<equiv>", 2)),
    1.28    ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),