summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 20 Oct 2016 19:39:27 +0200 | |

changeset 64323 | 20d15328b248 |

parent 64321 | 95be866e49fc (current diff) |

parent 64322 | 72060e61ca9d (diff) |

child 64328 | 2284011c341a |

tuned

NEWS | file | annotate | diff | comparison | revisions | |

src/HOL/ROOT | file | annotate | diff | comparison | revisions |

--- a/NEWS Thu Oct 20 18:42:01 2016 +0200 +++ b/NEWS Thu Oct 20 19:39:27 2016 +0200 @@ -281,6 +281,9 @@ mod_1 ~> mod_by_Suc_0 INCOMPATIBILITY. +* Renamed constants "setsum" ~> "sum" and "setprod" ~> "prod". + Corresponding renaming of theorems. + * New type class "idom_abs_sgn" specifies algebraic properties of sign and absolute value functions. Type class "sgn_if" has disappeared. Slight INCOMPATIBILITY.