444 Delimfix ("'(_')", "idt => idt", ""), |
444 Delimfix ("'(_')", "idt => idt", ""), |
445 Delimfix ("_", "idt => idts", ""), |
445 Delimfix ("_", "idt => idts", ""), |
446 Mixfix ("_/ _", "[idt, idts] => idts", "_idts", [1, 0], 0), |
446 Mixfix ("_/ _", "[idt, idts] => idts", "_idts", [1, 0], 0), |
447 Delimfix ("_", "id => aprop", ""), |
447 Delimfix ("_", "id => aprop", ""), |
448 Delimfix ("_", "var => aprop", ""), |
448 Delimfix ("_", "var => aprop", ""), |
449 Mixfix ("_'(_')", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0), |
449 Mixfix ("_/(1'(_'))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0), |
450 Delimfix ("PROP _", "aprop => prop", "_aprop"), |
450 Delimfix ("PROP _", "aprop => prop", "_aprop"), |
451 Delimfix ("_", "prop => asms", ""), |
451 Delimfix ("_", "prop => asms", ""), |
452 Delimfix ("_;/ _", "[prop, asms] => asms", "_asms"), |
452 Delimfix ("_;/ _", "[prop, asms] => asms", "_asms"), |
453 Mixfix ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1), |
453 Mixfix ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1), |
454 Mixfix ("(_ ==/ _)", "['a::{}, 'a] => prop", "==", [3, 2], 2), |
454 Mixfix ("(_ ==/ _)", "['a::{}, 'a] => prop", "==", [3, 2], 2), |