Re: [isabelle] Isabelle 2016 RC1: multiset changes

Hi Bertram,

2016-01-20 15:52 GMT+01:00 Bertram Felgenhauer via Cl-isabelle-users <
cl-isabelle-users at>:

> 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:

> 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,
> Bertram

Mathias Fleury

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