[isabelle-dev] Multiset insert
Jasmin Blanchette
jasmin.blanchette at inria.fr
Thu Jul 28 13:03:44 CEST 2016
> I would also like to point out that for some reason, intersection and union are #∪ and #∩, whereas all other multiset operations seem to have the # at the end (e.g. ⊆#). Unless there is some deeper reason for this, I suggest we change it.
Good point. Indeed, I first wrote ∪# in Isabelle when typing in the example from the previous email.
Unless there are objections, we will add that to our multiset cleanup list.
Jasmin
More information about the isabelle-dev
mailing list