*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isabelle2016-1-RC1: NEWS: setsum -> sum*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 2 Nov 2016 21:26:13 +0100*In-reply-to*: <33c8605d-baf6-32ae-00e8-b66d6a87d30b@inf.ethz.ch>*References*: <alpine.LNX.2.00.1601152117300.53323@lxbroy10.informatik.tu-muenchen.de> <55603fb1-2edb-84a9-9785-7da9359f488f@sketis.net> <33c8605d-baf6-32ae-00e8-b66d6a87d30b@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

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**

**Follow-Ups**:**Re: [isabelle] Isabelle2016-1-RC1: NEWS: setsum -> sum***From:*Makarius

**References**:**[isabelle] Isabelle2016-1-RC1: NEWS: setsum -> sum***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Mixing recursion and corecursion
- Next by Date: Re: [isabelle] Mixing recursion and corecursion
- Previous by Thread: [isabelle] Isabelle2016-1-RC1: NEWS: setsum -> sum
- Next by Thread: Re: [isabelle] Isabelle2016-1-RC1: NEWS: setsum -> sum
- Cl-isabelle-users November 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list