I've been using multisets quite a bit myself lately. add# and add1# both
sound all right to me.
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.
On 28/07/16 10:45, Florian Haftmann wrote:
However this is maybe now all too depp-rooted to consolidate it. Even
if not, alternatives have been proposed here that would resolve that
issue than.
‘depp-rooted’ is now my new favourite word. :D
Cheers,
Manuel
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
