[isabelle] Isabelle2016-1-RC1: NEWS: setsum -> sum



Hi all,

I noticed that NEWS is somewhat inconsistent about the renaming of theorems involving setsum. There's the general remark that setsum has been renamed to sum and that all theorems have changed their names accordingly. But a bit later, it says

  * The following theorems have been renamed:

    setsum_left_distrib ~> setsum_distrib_right
    setsum_right_distrib ~> setsum_distrib_left


This is no longer up-to-date, because one has to apply the renaming of setsum to the right-hand side again. I would find it less confusing if these lines were the following:

  * The following theorems have been renamed:

    setsum_left_distrib ~> sum_distrib_right
    setsum_right_distrib ~> sum_distrib_left

Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.