| changeset 54481 | 5c9819d7713b |
| parent 54477 | f001ef2637d3 |
| child 55023 | 38db7814481d |
| 54480:57e781b711b5 | 54481:5c9819d7713b |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* Well-Order Relations *} |
8 header {* Well-Order Relations *} |
9 |
9 |
10 theory Wellorder_Relation |
10 theory Wellorder_Relation |
11 imports Wellorder_Relation_LFP Wellfounded_More |
11 imports Wellorder_Relation_FP Wellfounded_More |
12 begin |
12 begin |
13 |
13 |
14 context wo_rel |
14 context wo_rel |
15 begin |
15 begin |
16 |
16 |