src/ZF/Main_ZF.thy
changeset 29580 117b88da143c
parent 26339 7825c83c9eff
child 36543 0e7fc5bf38de
equal deleted inserted replaced
29579:cb520b766e00 29580:117b88da143c
     1 (*$Id$*)
       
     2 
       
     3 header{*Theory Main: Everything Except AC*}
     1 header{*Theory Main: Everything Except AC*}
     4 
     2 
     5 theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin
     3 theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin
     6 
     4 
     7 (*The theory of "iterates" logically belongs to Nat, but can't go there because
     5 (*The theory of "iterates" logically belongs to Nat, but can't go there because