src/ZF/OrdQuant.thy
changeset 6093 87bf8c03b169
parent 3940 1d5bee4d047f
child 12114 a8e860c86252
     1.1 --- a/src/ZF/OrdQuant.thy	Tue Jan 12 13:54:51 1999 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Tue Jan 12 15:17:37 1999 +0100
     1.3 @@ -7,8 +7,6 @@
     1.4  
     1.5  OrdQuant = Ordinal +
     1.6  
     1.7 -global
     1.8 -
     1.9  consts
    1.10    
    1.11    (* Ordinal Quantifiers *)
    1.12 @@ -32,8 +30,6 @@
    1.13    "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
    1.14    "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
    1.15  
    1.16 -local
    1.17 -
    1.18  defs
    1.19    
    1.20    (* Ordinal Quantifiers *)