[isabelle-dev] Multiset insert

[Bertram Felgenhauer]

Tobias Nipkow wrote:
> 
> I am all in favour of a variation of "add" - it corresponds nicely to "+".
> Of course not "add" by itself, that is too generic. How about
> 
> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
> "add# x M = {#x#} + M"

I like "add#".

Will the introduction of add# mean that the induction principle for
multisets will be changed as well? If so, do you have a migration path
for proofs based on the current induction principle? (Currently there
are two cases, {#} and M + {#x#}; note that the singleton multiset
appears on the right, and given that Isabelle's simplifier is not very
good at handling AC symbols, changing the order has to potential to
break a lot of proofs).

Cheers,

Bertram