113 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, |
113 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, |
114 Sup_fun_def, Inf_apply, Sup_apply. |
114 Sup_fun_def, Inf_apply, Sup_apply. |
115 |
115 |
116 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary, |
116 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary, |
117 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter, |
117 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter, |
118 INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, |
118 INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset, |
119 UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been |
119 UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been |
120 discarded. |
120 discarded. |
121 |
121 |
122 More consistent and comprehensive names: |
122 More consistent and comprehensive names: |
123 |
123 |