[isabelle-dev] Explicit representation of multisets

Jasmin Blanchette jasmin.blanchette at inria.fr
Sun Mar 13 15:24:52 CET 2016

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


More information about the isabelle-dev mailing list