[isabelle-dev] Explicit representation of multisets

[Jasmin Blanchette]

> but this leads to the rather lengthy "insert_mset x M" as opposed to the current "{#x#} + M". This would come up in all inductive proofs. If we want to mimic sets, it actually seems unavoidable...

With completion, it might actually be easier to type "insert_mset x M" than "{#x#} + M". (The former is visually longer, for sure.)

Jasmin