[isabelle-dev] Multiset insert

[Peter Lammich]

On Do, 2016-07-28 at 10:21 +0200, Jasmin Blanchette wrote:
> Tobias wrote:
> 
> > How about
> > 
> > definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
> > "add# x M = {#x#} + M"

This, however, may produce confusion with multiset union, which is an
instance of the plus type classes, i.e., occupying the name
plus_multiset.

--
  Peter


> 
> Lovely!
> 
> Jasmin
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev