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