equal
deleted
inserted
replaced
278 mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] |
278 mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] |
279 zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric] |
279 zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric] |
280 div_1 ~> div_by_Suc_0 |
280 div_1 ~> div_by_Suc_0 |
281 mod_1 ~> mod_by_Suc_0 |
281 mod_1 ~> mod_by_Suc_0 |
282 INCOMPATIBILITY. |
282 INCOMPATIBILITY. |
|
283 |
|
284 * Renamed constants "setsum" ~> "sum" and "setprod" ~> "prod". |
|
285 Corresponding renaming of theorems. |
283 |
286 |
284 * New type class "idom_abs_sgn" specifies algebraic properties |
287 * New type class "idom_abs_sgn" specifies algebraic properties |
285 of sign and absolute value functions. Type class "sgn_if" has |
288 of sign and absolute value functions. Type class "sgn_if" has |
286 disappeared. Slight INCOMPATIBILITY. |
289 disappeared. Slight INCOMPATIBILITY. |
287 |
290 |