[isabelle-dev] Multiset insert
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