--- a/src/HOL/Library/Multiset.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Sep 30 20:30:59 2024 +0200
@@ -91,13 +91,10 @@
"\<lambda>a M b. if b = a then Suc (M b) else M b"
by (rule add_mset_in_multiset)
-nonterminal multiset_args
syntax
- "" :: "'a \<Rightarrow> multiset_args" (\<open>_\<close>)
- "_multiset_args" :: "'a \<Rightarrow> multiset_args \<Rightarrow> multiset_args" (\<open>_,/ _\<close>)
- "_multiset" :: "multiset_args \<Rightarrow> 'a multiset" (\<open>{#(_)#}\<close>)
+ "_multiset" :: "args \<Rightarrow> 'a multiset" (\<open>{#(\<open>notation=\<open>mixfix multiset enumeration\<close>\<close>_)#}\<close>)
syntax_consts
- "_multiset_args" "_multiset" == add_mset
+ add_mset
translations
"{#x, xs#}" == "CONST add_mset x {#xs#}"
"{#x#}" == "CONST add_mset x {#}"