Tobias wrote:
> How about
>
> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
> "add# x M = {#x#} + M"Lovely! Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
