equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {*Absoluteness for Order Types, Rank Functions and Well-Founded |
6 header {*Absoluteness for Order Types, Rank Functions and Well-Founded |
7 Relations*} |
7 Relations*} |
8 |
8 |
9 theory Rank = WF_absolute: |
9 theory Rank imports WF_absolute begin |
10 |
10 |
11 subsection {*Order Types: A Direct Construction by Replacement*} |
11 subsection {*Order Types: A Direct Construction by Replacement*} |
12 |
12 |
13 locale M_ordertype = M_basic + |
13 locale M_ordertype = M_basic + |
14 assumes well_ord_iso_separation: |
14 assumes well_ord_iso_separation: |