[isabelle-dev] Multiset insert

Manuel Eberl eberlm at in.tum.de
Thu Jul 28 11:52:42 CEST 2016

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



More information about the isabelle-dev mailing list