68 |
68 |
69 * Class complete_lattice: generalized a couple of lemmas from sets; |
69 * Class complete_lattice: generalized a couple of lemmas from sets; |
70 generalized theorems INF_cong and SUP_cong. New type classes for complete |
70 generalized theorems INF_cong and SUP_cong. New type classes for complete |
71 boolean algebras and complete linear orders. Lemmas Inf_less_iff, |
71 boolean algebras and complete linear orders. Lemmas Inf_less_iff, |
72 less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder. |
72 less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder. |
73 Changed proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply. |
73 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, Sup_fun_def, |
|
74 Inf_apply, Sup_apply. |
74 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary, |
75 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary, |
75 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter, |
76 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter, |
76 INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image, |
77 INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image, |
77 Union_def, UN_singleton, UN_eq have been discarded. |
78 Union_def, UN_singleton, UN_eq have been discarded. |
78 More consistent and less misunderstandable names: |
79 More consistent and less misunderstandable names: |