src/Pure/Syntax/sextension.ML
changeset 113 1e669b5a75f9
parent 48 bc48a71464b0
child 165 793be9f1e88e
equal deleted inserted replaced
112:009ae5c85ae9 113:1e669b5a75f9
   436       Delimfix ("'(_')",      "idt => idt",                    ""),
   436       Delimfix ("'(_')",      "idt => idt",                    ""),
   437       Delimfix ("_",          "idt => idts",                   ""),
   437       Delimfix ("_",          "idt => idts",                   ""),
   438       Mixfix   ("_/ _",       "[idt, idts] => idts",           "_idts", [1, 0], 0),
   438       Mixfix   ("_/ _",       "[idt, idts] => idts",           "_idts", [1, 0], 0),
   439       Delimfix ("_",          "id => aprop",                   ""),
   439       Delimfix ("_",          "id => aprop",                   ""),
   440       Delimfix ("_",          "var => aprop",                  ""),
   440       Delimfix ("_",          "var => aprop",                  ""),
   441       Mixfix   ("_/(1'(_'))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0),
   441       Mixfix   ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0),
   442       Delimfix ("PROP _",     "aprop => prop",                 "_aprop"),
   442       Delimfix ("PROP _",     "aprop => prop",                 "_aprop"),
   443       Delimfix ("_",          "prop => asms",                  ""),
   443       Delimfix ("_",          "prop => asms",                  ""),
   444       Delimfix ("_;/ _",      "[prop, asms] => asms",          "_asms"),
   444       Delimfix ("_;/ _",      "[prop, asms] => asms",          "_asms"),
   445       Mixfix   ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1),
   445       Mixfix   ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1),
   446       Mixfix   ("(_ ==/ _)",  "['a::{}, 'a] => prop",          "==", [3, 2], 2),
   446       Mixfix   ("(_ ==/ _)",  "['a::{}, 'a] => prop",          "==", [3, 2], 2),