equal
deleted
inserted
replaced
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 header{*Order Types and Ordinal Arithmetic*} |
8 header{*Order Types and Ordinal Arithmetic*} |
9 |
9 |
10 theory OrderType = OrderArith + OrdQuant + Nat: |
10 theory OrderType imports OrderArith OrdQuant Nat begin |
11 |
11 |
12 text{*The order type of a well-ordering is the least ordinal isomorphic to it. |
12 text{*The order type of a well-ordering is the least ordinal isomorphic to it. |
13 Ordinal arithmetic is traditionally defined in terms of order types, as it is |
13 Ordinal arithmetic is traditionally defined in terms of order types, as it is |
14 here. But a definition by transfinite recursion would be much simpler!*} |
14 here. But a definition by transfinite recursion would be much simpler!*} |
15 |
15 |