should have been copied across from Set.thy as well for better printing
authornipkow
Wed, 03 Jun 2020 11:44:21 +0200
changeset 72144 4c5778d8a53d
parent 72143 435cdc772110
child 72145 4e0a58818edc
should have been copied across from Set.thy as well for better printing
src/HOL/Library/Multiset.thy
--- 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)