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), |