| changeset 26056 | 6a0801279f4c |
| parent 24893 | b8ef7afe3a6b |
| child 32960 | 69916a850301 |
--- a/src/ZF/OrderType.thy Mon Feb 11 15:19:17 2008 +0100 +++ b/src/ZF/OrderType.thy Mon Feb 11 15:40:21 2008 +0100 @@ -7,7 +7,7 @@ header{*Order Types and Ordinal Arithmetic*} -theory OrderType imports OrderArith OrdQuant Nat begin +theory OrderType imports OrderArith OrdQuant Nat_ZF begin text{*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