Email Gateway (Aug 22 2022 at 14:26): Email Gateway (Aug 22 2022 at 14:26):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 14:28):From: Tobias Nipkow <nipkow@in.tum.de>
Indeed, that would be better.
Thanks
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 14:32):From: Makarius <makarius@sketis.net>
That has become change cc2da001465b on the isabelle-dev repository, but
anything for Isabelle2016-1 needs to go to the isabelle-release
repository, by sending changesets to me by mail.
I have applied that change already by "cherry-picking" it, see
https://bitbucket.org/isabelle_project/isabelle-release/commits/f7aa4d0f7d0,
but this principle does not work well when the two repositories diverge
further in the coming weeks.
Changes should normally go either on isabelle-dev (post-release
development) or on isabelle-release (important amendments of release
candidate material).
Makarius
Last updated: Apr 25 2024 at 20:15 UTC