Email Gateway (Aug 22 2022 at 14:25): Email Gateway (Aug 22 2022 at 14:25):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
after more than 2 weeks, here is the next release candidate for
Isabelle2016-1 (December 2016):
http://isabelle.in.tum.de/website-Isabelle2016-1-RC3 -- see also
http://sketis.net/2016/release-candidates-for-isabelle2016-1.
More fine points have been consolidated. A component for the new
experimental Nunchaku tool has been included.
The corresponding repository versions of Isabelle and AFP are
https://bitbucket.org/isabelle_project/isabelle-release/commits/8bf3d0553c35
and https://bitbucket.org/isa-afp/afp-devel/commits/1a3901597f0f
It is also possible to follow nightly development snapshots from
http://isabelle.in.tum.de/devel although they might be somewhat erratic.
At this stage, Isabelle release candidates are already sufficiently
consolidated to be ready for everyday use. Adapting your applications
now gives a unique chance for feedback before the release is finalized.
When discussing problems, observations, suggestions, etc. the mail
subject line should be changed to something informative, and the
particular Isabelle version given in the message body.
Makarius
Email Gateway (Aug 22 2022 at 14:26):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Makarius wrote:
One of the big changes concerns multisets. In the multiset
extension theory, there is a cancellation law
(X + Z <ms Y + Z implies X <ms Y), but no corresponding variant
for add_mset. Is it too late add this? It would be:
lemmas mult_cancel1 = mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right]
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 14:26):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Bertram Felgenhauer via Cl-isabelle-users wrote:
Sorry, it should be
lemmas mult_cancel1 = mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right empty_neutral]
(I had used simplified, and didn't spot the lingering empty multiset)
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 14:27):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Bertram,
I guess we could add it. However, to what extent is this a critical issue that needs to be resolved before the release, as opposed to after? I believe that IsaFoR already contains a theory file full with multiset lemmas. My suggestion would be for you to add it there, and for us (the Isabelle developers), to add it in the development version of Isabelle (i.e. for Isabelle2017). Unless it is more critical than it looks like.
(Getting closer to a release, it makes sense to become more and more conservative in the changes we incorporate. Otherwise, we'll never converge.)
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 14:29):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Jasmin Blanchette wrote:
You're right, it's not critical.
Cheers,
Bertram
Last updated: Apr 25 2024 at 04:18 UTC