src/ZF/OrdQuant.thy
changeset 12552 d2d2ab3f1f37
parent 12114 a8e860c86252
child 12620 4e6626725e21
     1.1 --- a/src/ZF/OrdQuant.thy	Wed Dec 19 11:07:38 2001 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Wed Dec 19 11:13:27 2001 +0100
     1.3 @@ -26,9 +26,9 @@
     1.4    "UN x<a. B"   == "OUnion(a, %x. B)"
     1.5  
     1.6  syntax (xsymbols)
     1.7 -  "@oall"     :: [idt, i, o] => o        ("(3\\<forall> _<_./ _)" 10)
     1.8 -  "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
     1.9 -  "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
    1.10 +  "@oall"     :: [idt, i, o] => o        ("(3\\<forall>_<_./ _)" 10)
    1.11 +  "@oex"      :: [idt, i, o] => o        ("(3\\<exists>_<_./ _)" 10)
    1.12 +  "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union>_<_./ _)" 10)
    1.13  
    1.14  defs
    1.15