equal
deleted
inserted
replaced
132 |
132 |
133 * The simplifier uses image_cong_simp as a congruence rule. The historic |
133 * The simplifier uses image_cong_simp as a congruence rule. The historic |
134 and not really well-formed congruence rules INF_cong*, SUP_cong*, |
134 and not really well-formed congruence rules INF_cong*, SUP_cong*, |
135 are not used by default any longer. INCOMPATIBILITY; consider using |
135 are not used by default any longer. INCOMPATIBILITY; consider using |
136 declare image_cong_simp [cong del] in extreme situations. |
136 declare image_cong_simp [cong del] in extreme situations. |
|
137 |
|
138 * INF_image and SUP_image are no default simp rules any longer. |
|
139 INCOMPATIBILITY, prefer image_comp as simp rule if needed. |
137 |
140 |
138 * Simplified syntax setup for big operators under image. In rare |
141 * Simplified syntax setup for big operators under image. In rare |
139 situations, type conversions are not inserted implicitly any longer |
142 situations, type conversions are not inserted implicitly any longer |
140 and need to be given explicitly. Auxiliary abbreviations INFIMUM, |
143 and need to be given explicitly. Auxiliary abbreviations INFIMUM, |
141 SUPREMUM, UNION, INTER should now rarely occur in output and are just |
144 SUPREMUM, UNION, INTER should now rarely occur in output and are just |