--- a/src/HOL/Library/Multiset.thy Sat May 30 11:48:35 2020 +0000
+++ b/src/HOL/Library/Multiset.thy Wed Jun 03 11:44:21 2020 +0200
@@ -189,6 +189,11 @@
"\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
"\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
+print_translation \<open>
+ [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Ball\<close> \<^syntax_const>\<open>_MBall\<close>,
+ Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Bex\<close> \<^syntax_const>\<open>_MBex\<close>]
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+
lemma count_eq_zero_iff:
"count M x = 0 \<longleftrightarrow> x \<notin># M"
by (auto simp add: set_mset_def)