[isabelle-dev] Multiset insert
Jasmin Blanchette
jasmin.blanchette at inria.fr
Thu Jul 28 10:21:58 CEST 2016
Tobias wrote:
> How about
>
> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
> "add# x M = {#x#} + M"
Lovely!
Jasmin
More information about the isabelle-dev
mailing list