equal
deleted
inserted
replaced
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 Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply. |
|
71 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary and Sup_binary have |
|
72 been discarded. |
71 More consistent and less misunderstandable names: |
73 More consistent and less misunderstandable names: |
72 INFI_def ~> INF_def |
74 INFI_def ~> INF_def |
73 SUPR_def ~> SUP_def |
75 SUPR_def ~> SUP_def |
74 le_SUPI ~> le_SUP_I |
76 le_SUPI ~> le_SUP_I |
75 le_SUPI2 ~> le_SUP_I2 |
77 le_SUPI2 ~> le_SUP_I2 |