src/Pure/Syntax/mixfix.ML
changeset 3829 d7333ef9e72c
parent 3815 7e8847f8f3a4
child 4053 c88d0d5ae806
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Oct 10 15:46:50 1997 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Oct 10 15:47:41 1997 +0200
     1.3 @@ -172,6 +172,7 @@
     1.4    ("",             "pttrn => pttrns",               Delimfix "_"),
     1.5    ("_pttrns",      "[pttrn, pttrns] => pttrns",     Mixfix ("_/ _", [1, 0], 0)),
     1.6    ("",             "id => aprop",                   Delimfix "_"),
     1.7 +  ("",             "longid => aprop",               Delimfix "_"),
     1.8    ("",             "var => aprop",                  Delimfix "_"),
     1.9    ("_aprop",       "aprop => prop",                 Delimfix "PROP _"),
    1.10    ("",             "prop => asms",                  Delimfix "_"),
    1.11 @@ -182,6 +183,7 @@
    1.12    ("_mk_ofclassS", "_",                             NoSyn),
    1.13    ("_K",           "_",                             NoSyn),
    1.14    ("",             "id => logic",                   Delimfix "_"),
    1.15 +  ("",             "longid => logic",               Delimfix "_"),
    1.16    ("",             "var => logic",                  Delimfix "_")];
    1.17  
    1.18  val pure_appl_syntax =
    1.19 @@ -206,4 +208,5 @@
    1.20    ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
    1.21    ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
    1.22  
    1.23 +
    1.24  end;