>> 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
