changeset 26056 | 6a0801279f4c |
parent 24893 | b8ef7afe3a6b |
child 32960 | 69916a850301 |
--- a/src/ZF/Cardinal.thy Mon Feb 11 15:19:17 2008 +0100 +++ b/src/ZF/Cardinal.thy Mon Feb 11 15:40:21 2008 +0100 @@ -7,7 +7,7 @@ header{*Cardinal Numbers Without the Axiom of Choice*} -theory Cardinal imports OrderType Finite Nat Sum begin +theory Cardinal imports OrderType Finite Nat_ZF Sum begin definition (*least ordinal operator*)