> 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