[isabelle-dev] Multiset insert

[Manuel Eberl]

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