Re: [isabelle] Isabelle 2016 RC1: multiset changes



Hi Bertram,

I am sorry I misread your second question.

To be more clear about the symbols (in red the changes compared to previous year):

           multiset inclusion    multiset ordering
2014         <  and â                   <# and  â#
2015         < and â                    #<# and #â#
2016        <# and â#                #<# and #â#
2016.1     <# and â#                 < and â  (expected)

So it is not a mistake in the NEWS file.



About your second question, it is an oversight: we completely forget the > symbols. Jasmin will add them soon (before the next RC).


Sorry about my misreading,
Mathias



> On 20 Jan 2016, at 16:30, Fleury Mathias <mathias.fleury12 at gmail.com> wrote:
> 
> Hi Bertram,
> 
> 
> 2016-01-20 15:52 GMT+01:00 Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk <mailto:cl-isabelle-users at lists.cam.ac.uk>>:
> Hi,
> 
> in commit f8a513fedb31, multiset inclusion was changed from an instance
> of order to a set of custom orders. I'm wondering why this was done.
> (This is not a complaint, but I didn't find any discussion about this.)
>  
> There were some discussions 10 months ago: http://fa.isabelle.narkive.com/Lv0NWbCa/isabelle-multiset-ordering-vs-subset-syntaxÂ; <http://fa.isabelle.narkive.com/Lv0NWbCa/isabelle-multiset-ordering-vs-subset-syntax>
> 
>  
> 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>#.
> 
> 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). 
>  
> 
> Cheers,
> Mathias
>  
> 
> Cheers,
> 
> Bertram
> 
> 
> 
> 
> 
> -- 
> Mathias Fleury
> MPI - INF




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.