equal
deleted
inserted
replaced
3 Copyright 2012 |
3 Copyright 2012 |
4 |
4 |
5 Well-order relations as needed by bounded natural functors. |
5 Well-order relations as needed by bounded natural functors. |
6 *) |
6 *) |
7 |
7 |
8 header {* Well-Order Relations as Needed by Bounded Natural Functors *} |
8 section {* Well-Order Relations as Needed by Bounded Natural Functors *} |
9 |
9 |
10 theory BNF_Wellorder_Relation |
10 theory BNF_Wellorder_Relation |
11 imports Order_Relation |
11 imports Order_Relation |
12 begin |
12 begin |
13 |
13 |