| changeset 55056 | b5c94200d081 |
| parent 55023 | 38db7814481d |
| child 55102 | 761e40ce91bc |
| 55055:3f0dfce0e27a | 55056:b5c94200d081 |
|---|---|
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_FP Wellfounded_More |
11 imports BNF_Wellorder_Relation Wellfounded_More |
12 begin |
12 begin |
13 |
13 |
14 context wo_rel |
14 context wo_rel |
15 begin |
15 begin |
16 |
16 |