[isabelle-dev] Multiset insert

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160728/e0337085/attachment.sig>