> 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
