[isabelle-dev] Multiset insert

[Jasmin Blanchette]

Hi Bertram,

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

I guess it would make sense to keep the other principle around for compatibility. However, even if we didn't, it would be almost trivial to derive one principle from the other -- so you could always do that on your side instead of adapting the proofs.

Cheers,

Jasmin