| changeset 54473 | 8bee5ca99e63 |
| parent 49310 | 6e30078de4f0 |
| child 54481 | 5c9819d7713b |
| 54472:073f041d83ae | 54473:8bee5ca99e63 |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* More on Well-Founded Relations *} |
8 header {* More on Well-Founded Relations *} |
9 |
9 |
10 theory Wellfounded_More |
10 theory Wellfounded_More |
11 imports Wellfounded_More_Base Order_Relation_More |
11 imports Wellfounded_More_LFP Order_Relation_More |
12 begin |
12 begin |
13 |
13 |
14 |
14 |
15 subsection {* Well-founded recursion via genuine fixpoints *} |
15 subsection {* Well-founded recursion via genuine fixpoints *} |
16 |
16 |