changeset 12114 | a8e860c86252 |
parent 6093 | 87bf8c03b169 |
child 12552 | d2d2ab3f1f37 |
--- a/src/ZF/OrdQuant.thy Fri Nov 09 00:06:15 2001 +0100 +++ b/src/ZF/OrdQuant.thy Fri Nov 09 00:09:47 2001 +0100 @@ -25,7 +25,7 @@ "EX x<a. P" == "oex(a, %x. P)" "UN x<a. B" == "OUnion(a, %x. B)" -syntax (symbols) +syntax (xsymbols) "@oall" :: [idt, i, o] => o ("(3\\<forall> _<_./ _)" 10) "@oex" :: [idt, i, o] => o ("(3\\<exists> _<_./ _)" 10) "@OUNION" :: [idt, i, i] => i ("(3\\<Union> _<_./ _)" 10)