changeset 68490 | eb53f944c8cd |
parent 63648 | f9f3006a5579 |
child 69587 | 53982d5ec0bb |
--- a/src/ZF/OrderType.thy Sun Jun 24 11:41:41 2018 +0100 +++ b/src/ZF/OrderType.thy Sun Jun 24 15:57:48 2018 +0200 @@ -5,7 +5,7 @@ section\<open>Order Types and Ordinal Arithmetic\<close> -theory OrderType imports OrderArith OrdQuant Nat_ZF begin +theory OrderType imports OrderArith OrdQuant Nat begin text\<open>The order type of a well-ordering is the least ordinal isomorphic to it. Ordinal arithmetic is traditionally defined in terms of order types, as it is