equal
deleted
inserted
replaced
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 Main |
11 imports Main |
12 begin |
12 begin |
13 |
|
14 |
13 |
15 subsection {* The upper and lower bounds operators *} |
14 subsection {* The upper and lower bounds operators *} |
16 |
15 |
17 lemma aboveS_subset_above: "aboveS r a \<le> above r a" |
16 lemma aboveS_subset_above: "aboveS r a \<le> above r a" |
18 by(auto simp add: aboveS_def above_def) |
17 by(auto simp add: aboveS_def above_def) |