Tobias wrote:
> Did we ever discuss the naming issue? "insert_mset" would be the canonical
> name, but it would make larger expressions hard to read.
I'm not so sure "insert_mset" would be the right name. Its set-based
terminology might suggest a definition like
insert_mset x M = {#x#} #∪ M
i.e. with #∪ instead of +. How about "add"?
add x M = {#x#} + M
Or "add1"? Or "add_mset" etc.?
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
