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