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 Changed 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 |
71 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary, |
72 been discarded. |
72 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter, |
|
73 INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image, |
|
74 Union_def, UN_singleton, UN_eq have been discarded. |
73 More consistent and less misunderstandable names: |
75 More consistent and less misunderstandable names: |
74 INFI_def ~> INF_def |
76 INFI_def ~> INF_def |
75 SUPR_def ~> SUP_def |
77 SUPR_def ~> SUP_def |
76 le_SUPI ~> le_SUP_I |
78 INF_leI ~> INF_lower |
77 le_SUPI2 ~> le_SUP_I2 |
79 INF_leI2 ~> INF_lower2 |
78 le_INFI ~> le_INF_I |
80 le_INFI ~> INF_greatest |
|
81 le_SUPI ~> SUP_upper |
|
82 le_SUPI2 ~> SUP_upper2 |
|
83 SUP_leI ~> SUP_least |
79 INFI_bool_eq ~> INF_bool_eq |
84 INFI_bool_eq ~> INF_bool_eq |
80 SUPR_bool_eq ~> SUP_bool_eq |
85 SUPR_bool_eq ~> SUP_bool_eq |
81 INFI_apply ~> INF_apply |
86 INFI_apply ~> INF_apply |
82 SUPR_apply ~> SUP_apply |
87 SUPR_apply ~> SUP_apply |
|
88 INTER_def ~> INTER_eq |
|
89 UNION_def ~> UNION_eq |
|
90 |
83 INCOMPATIBILITY. |
91 INCOMPATIBILITY. |
84 |
92 |
85 * Theorem collections ball_simps and bex_simps do not contain theorems referring |
93 * Theorem collections ball_simps and bex_simps do not contain theorems referring |
86 to UNION any longer; these have been moved to collection UN_ball_bex_simps. |
94 to UNION any longer; these have been moved to collection UN_ball_bex_simps. |
87 INCOMPATIBILITY. |
95 INCOMPATIBILITY. |