| changeset 68652 | 1e37b45ce3fb |
| parent 66453 | cc19f7ca2ed6 |
| child 76948 | f33df7529fed |
| 68648:371e814af6f0 | 68652:1e37b45ce3fb |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 section \<open>Well-Order Relations\<close> |
8 section \<open>Well-Order Relations\<close> |
9 |
9 |
10 theory Wellorder_Relation |
10 theory Wellorder_Relation |
11 imports HOL.BNF_Wellorder_Relation Wellfounded_More |
11 imports Wellfounded_More |
12 begin |
12 begin |
13 |
13 |
14 context wo_rel |
14 context wo_rel |
15 begin |
15 begin |
16 |
16 |