*To*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>*Subject*: Re: [isabelle] Isabelle 2016 RC1: multiset changes*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Wed, 20 Jan 2016 18:17:50 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20160120164257.GB20972@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>*References*: <20160120145250.GA20972@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f> <CAG2fU9jhLcW3x8Uwfn2fTqGqWPMU=EApWM+Qgm_Wz_wqm60vAQ@mail.gmail.com> <20160120164257.GB20972@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>

Hi Bertram, I'll take over, together with Mathias, to avoid further confusion (hopefully). ;) > So the motivation for the change is to make the multiset extension of an order on the elements the standard order for multisets. That's the main motivation, to allow nested multiset orders gracefully, among others. In addition, several people found the old (pre-Isabelle2014) notations confusing (especially \<subset># for the multiset order). > My mistake, \<subset># is just an alias for <#... so perhaps the former > two symbols should be < and \<ge>. (We don't entirely understand the last part of this sentence. "Former" and "should be" can mean many things.) > The point is that \<subset> and \<subseteq> do not work for multisets in Isabelle2015; We take this as meaning that the NEWS item is wrong. Indeed, it refers to some operators that don't exist in Isabelle2015. This will be fixed in the next release candidate. >> You can re-instantiate the multiset to be of sort ord (see for example >> ~~/src/HOL/UNITY/Follows.thy where this is done for the multiset ordering). >> However, I do not think that introducing abbreviations would be a good idea >> (issues would appear after the next release). > > What are those issues? As far as I understand, the relations <#, <=# > and \<le># will not be touched again. To be clear, I'm talking about > adding See Mathias's second email. Unfortunately, his little table, which we had concocted together based on our recollection, was slightly wrong. Here is an updated one. multiset inclusion multiset ordering 2014 < <# â# 2015 â# <# < #<# #â# 2016 â# <# #<# #â# 2016-1 (expected) â# (and <#?) < I hope this clears up the confusion. One of our goals is that people who know what < and \<subset> mean for sets can reuse that knowledge with multisets, but with the usual # suffix. Cheers, Jasmin & Mathias

**Follow-Ups**:**Re: [isabelle] Isabelle 2016 RC1: multiset changes***From:*Bertram Felgenhauer via Cl-isabelle-users

**References**:**[isabelle] Isabelle 2016 RC1: multiset changes***From:*Bertram Felgenhauer via Cl-isabelle-users

**Re: [isabelle] Isabelle 2016 RC1: multiset changes***From:*Fleury Mathias

**Re: [isabelle] Isabelle 2016 RC1: multiset changes***From:*Bertram Felgenhauer via Cl-isabelle-users

- Previous by Date: Re: [isabelle] Isabelle 2016 RC1: multiset changes
- Next by Date: [isabelle] RC1 - Greyout
- Previous by Thread: Re: [isabelle] Isabelle 2016 RC1: multiset changes
- Next by Thread: Re: [isabelle] Isabelle 2016 RC1: multiset changes
- Cl-isabelle-users January 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