equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Well-Order Relations (FP) *} |
8 header {* Well-Order Relations (FP) *} |
9 |
9 |
10 theory Wellorder_Relation_FP |
10 theory Wellorder_Relation_FP |
11 imports Wellfounded_More_FP |
11 imports Order_Relation |
12 begin |
12 begin |
13 |
13 |
14 |
14 |
15 text{* In this section, we develop basic concepts and results pertaining |
15 text{* In this section, we develop basic concepts and results pertaining |
16 to well-order relations. Note that we consider well-order relations |
16 to well-order relations. Note that we consider well-order relations |