30 "! " :: [idts, bool] => bool ("'((3forall _./ _)')" [0, 10] 10) |
30 "! " :: [idts, bool] => bool ("'((3forall _./ _)')" [0, 10] 10) |
31 "? " :: [idts, bool] => bool ("'((3exists _./ _)')" [0, 10] 10) |
31 "? " :: [idts, bool] => bool ("'((3exists _./ _)')" [0, 10] 10) |
32 "ALL " :: [idts, bool] => bool ("'((3forall _./ _)')" [0, 10] 10) |
32 "ALL " :: [idts, bool] => bool ("'((3forall _./ _)')" [0, 10] 10) |
33 "EX " :: [idts, bool] => bool ("'((3exists _./ _)')" [0, 10] 10) |
33 "EX " :: [idts, bool] => bool ("'((3exists _./ _)')" [0, 10] 10) |
34 |
34 |
35 "_lambda" :: [idts, 'a::logic] => 'b::logic ("(3L _./ _)" 10) |
35 "_lambda" :: [idts, 'a] => 'b ("(3L _./ _)" 10) |
36 "_applC" :: [('b => 'a), cargs] => aprop ("(1_/ '(_'))" [1000,1000] 999) |
36 "_applC" :: [('b => 'a), cargs] => aprop ("(1_/ '(_'))" [1000,1000] 999) |
37 "_cargs" :: ['a, cargs] => cargs ("_,/ _" [1000,1000] 1000) |
37 "_cargs" :: ['a, cargs] => cargs ("_,/ _" [1000,1000] 1000) |
38 |
38 |
39 "_idts" :: [idt, idts] => idts ("_,/ _" [1, 0] 0) |
39 "_idts" :: [idt, idts] => idts ("_,/ _" [1, 0] 0) |
40 |
40 |