*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isabelle 2016 RC1: multiset changes*From*: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Wed, 20 Jan 2016 17:42:58 +0100*In-reply-to*: <CAG2fU9jhLcW3x8Uwfn2fTqGqWPMU=EApWM+Qgm_Wz_wqm60vAQ@mail.gmail.com>*References*: <20160120145250.GA20972@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f> <CAG2fU9jhLcW3x8Uwfn2fTqGqWPMU=EApWM+Qgm_Wz_wqm60vAQ@mail.gmail.com>*Reply-to*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>*User-agent*: Mutt/1.5.24 (2015-08-30)

Hi Matthias, Thanks for your reply. I had not found the earlier discussion in my search (I only checked back to May 2015; I should have dug a little deeper). So the motivation for the change is to make the multiset extension of an order on the elements the standard order for multisets. > > I noticed that the NEWS entry mentions that \<subset> and \<subseteq> > > were changed to \<subset># and \<subseteq>#; I believe the former > > should be #\<subset># and #\<subseteq>#. My mistake, \<subset># is just an alias for <#... so perhaps the former two symbols should be < and \<ge>. The point is that \<subset> and \<subseteq> do not work for multisets in Isabelle2015; they are restricted to sets. This also applies to your next paragraph: > So far, there are two different orders over multisets: the multiset > inclusion (Isabelle2015: â, Isabelle2016: â#) and the multiset ordering > (since Isabelle2015: #â#). The long-term goal is to swap the symbols: â > should be the multiset ordering and not as previously the multiset > inclusion. We did not want to swap the two ordering in a single release > (too hard for users). > > Would it be possible to add abbreviations >#, >=# and \<ge># corresponding > > to the existing (in Isabelle 2015) abbreviations >, >= and \<ge> for ord? > > 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 abbreviation (input) supseteq_mset (infix ">#" 50) where "x ># y == y <# x" etc. Cheers, Bertram

**Follow-Ups**:**Re: [isabelle] Isabelle 2016 RC1: multiset changes***From:*Jasmin Blanchette

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

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

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