>> 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.
To a certain extent, maybe. The plus type class has (among other syntactic type classes) the historic defect that type class and operation are named »plus« whereas properties refer to »add«. To which I have contributed since I chose »plus« etc. when giving those operations proper names back in 2005 / 2006 / 2007. 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. Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev