| changeset 53336 | d25fc4c0ff62 |
| parent 53328 | 636b62eb7e88 |
| child 55846 | 8bee5ca99e63 |
| 53334:20071aef2a3b | 53336:d25fc4c0ff62 |
|---|---|
1 (* Title: HOL/Library/Order_Union.thy |
1 (* Title: HOL/Library/Order_Union.thy |
2 Author: Andrei Popescu, TU Muenchen |
2 Author: Andrei Popescu, TU Muenchen |
3 |
3 |
4 Subset of Constructions_on_Wellorders that provides the ordinal sum but does |
4 The ordinal-like sum of two orders with disjoint fields |
5 not rely on the ~/HOL/Library/Zorn.thy. |
|
6 *) |
5 *) |
7 |
6 |
8 header {* Order Union *} |
7 header {* Order Union *} |
9 |
8 |
10 theory Order_Union |
9 theory Order_Union |