equal
deleted
inserted
replaced
65 |
65 |
66 * Class complete_lattice: generalized a couple of lemmas from sets; |
66 * Class complete_lattice: generalized a couple of lemmas from sets; |
67 generalized theorems INF_cong and SUP_cong. New type classes for complete |
67 generalized theorems INF_cong and SUP_cong. New type classes for complete |
68 boolean algebras and complete linear orders. Lemmas Inf_less_iff, |
68 boolean algebras and complete linear orders. Lemmas Inf_less_iff, |
69 less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder. |
69 less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder. |
|
70 Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply. |
70 More consistent and less misunderstandable names: |
71 More consistent and less misunderstandable names: |
71 INFI_def ~> INF_def |
72 INFI_def ~> INF_def |
72 SUPR_def ~> SUP_def |
73 SUPR_def ~> SUP_def |
73 le_SUPI ~> le_SUP_I |
74 le_SUPI ~> le_SUP_I |
74 le_SUPI2 ~> le_SUP_I2 |
75 le_SUPI2 ~> le_SUP_I2 |