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-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
