changeset 16417 | 9bc16273c2d4 |
parent 14864 | 419b45cdb400 |
child 24826 | 78e6a3cea367 |
1.1 --- a/src/ZF/OrderType.thy Fri Jun 17 11:35:35 2005 +0200 1.2 +++ b/src/ZF/OrderType.thy Fri Jun 17 16:12:49 2005 +0200 1.3 @@ -7,7 +7,7 @@ 1.4 1.5 header{*Order Types and Ordinal Arithmetic*} 1.6 1.7 -theory OrderType = OrderArith + OrdQuant + Nat: 1.8 +theory OrderType imports OrderArith OrdQuant Nat begin 1.9 1.10 text{*The order type of a well-ordering is the least ordinal isomorphic to it. 1.11 Ordinal arithmetic is traditionally defined in terms of order types, as it is