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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
