equal
deleted
inserted
replaced
24 "ALL x<a. P" == "oall(a, %x. P)" |
24 "ALL x<a. P" == "oall(a, %x. P)" |
25 "EX x<a. P" == "oex(a, %x. P)" |
25 "EX x<a. P" == "oex(a, %x. P)" |
26 "UN x<a. B" == "OUnion(a, %x. B)" |
26 "UN x<a. B" == "OUnion(a, %x. B)" |
27 |
27 |
28 syntax (xsymbols) |
28 syntax (xsymbols) |
29 "@oall" :: [idt, i, o] => o ("(3\\<forall> _<_./ _)" 10) |
29 "@oall" :: [idt, i, o] => o ("(3\\<forall>_<_./ _)" 10) |
30 "@oex" :: [idt, i, o] => o ("(3\\<exists> _<_./ _)" 10) |
30 "@oex" :: [idt, i, o] => o ("(3\\<exists>_<_./ _)" 10) |
31 "@OUNION" :: [idt, i, i] => i ("(3\\<Union> _<_./ _)" 10) |
31 "@OUNION" :: [idt, i, i] => i ("(3\\<Union>_<_./ _)" 10) |
32 |
32 |
33 defs |
33 defs |
34 |
34 |
35 (* Ordinal Quantifiers *) |
35 (* Ordinal Quantifiers *) |
36 oall_def "oall(A, P) == ALL x. x<A --> P(x)" |
36 oall_def "oall(A, P) == ALL x. x<A --> P(x)" |