src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -93,6 +93,8 @@
 
 syntax
   "_multiset" :: "args \<Rightarrow> 'a multiset"  (\<open>(\<open>indent=2 notation=\<open>mixfix multiset enumeration\<close>\<close>{#_#})\<close>)
+syntax_consts
+  "_multiset" \<rightleftharpoons> add_mset
 translations
   "{#x, xs#}" == "CONST add_mset x {#xs#}"
   "{#x#}" == "CONST add_mset x {#}"