equal
deleted
inserted
replaced
26 text{* The following context encompasses all this section. In other words, |
26 text{* The following context encompasses all this section. In other words, |
27 for the whole section, we consider a fixed well-order relation @{term "r"}. *} |
27 for the whole section, we consider a fixed well-order relation @{term "r"}. *} |
28 |
28 |
29 (* context wo_rel *) |
29 (* context wo_rel *) |
30 |
30 |
31 abbreviation under where "under \<equiv> Order_Relation_More_FP.under r" |
31 abbreviation under where "under \<equiv> Order_Relation.under r" |
32 abbreviation underS where "underS \<equiv> Order_Relation_More_FP.underS r" |
32 abbreviation underS where "underS \<equiv> Order_Relation.underS r" |
33 abbreviation Under where "Under \<equiv> Order_Relation_More_FP.Under r" |
33 abbreviation Under where "Under \<equiv> Order_Relation.Under r" |
34 abbreviation UnderS where "UnderS \<equiv> Order_Relation_More_FP.UnderS r" |
34 abbreviation UnderS where "UnderS \<equiv> Order_Relation.UnderS r" |
35 abbreviation above where "above \<equiv> Order_Relation_More_FP.above r" |
35 abbreviation above where "above \<equiv> Order_Relation.above r" |
36 abbreviation aboveS where "aboveS \<equiv> Order_Relation_More_FP.aboveS r" |
36 abbreviation aboveS where "aboveS \<equiv> Order_Relation.aboveS r" |
37 abbreviation Above where "Above \<equiv> Order_Relation_More_FP.Above r" |
37 abbreviation Above where "Above \<equiv> Order_Relation.Above r" |
38 abbreviation AboveS where "AboveS \<equiv> Order_Relation_More_FP.AboveS r" |
38 abbreviation AboveS where "AboveS \<equiv> Order_Relation.AboveS r" |
39 |
39 |
40 |
40 |
41 subsection {* Auxiliaries *} |
41 subsection {* Auxiliaries *} |
42 |
42 |
43 |
43 |