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



Indeed, that would be better.

Thanks
Tobias

On 02/11/2016 18:31, Andreas Lochbihler wrote:
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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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