| changeset 54481 | 5c9819d7713b |
| parent 54479 | af1ea7ca7417 |
| child 54552 | 5d57cbec0f0f |
| 54480:57e781b711b5 | 54481:5c9819d7713b |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* Basics on Order-Like Relations *} |
8 header {* Basics on Order-Like Relations *} |
9 |
9 |
10 theory Order_Relation_More |
10 theory Order_Relation_More |
11 imports Order_Relation_More_LFP |
11 imports Order_Relation_More_FP |
12 begin |
12 begin |
13 |
13 |
14 |
14 |
15 subsection {* The upper and lower bounds operators *} |
15 subsection {* The upper and lower bounds operators *} |
16 |
16 |