src/HOL/Library/Multiset.thy
changeset 64587 8355a6e2df79
parent 64586 1d25ca718790
child 64591 240a39af9ec4
     1.1 --- a/src/HOL/Library/Multiset.thy	Sat Dec 17 15:22:00 2016 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Dec 17 15:22:13 2016 +0100
     1.3 @@ -528,7 +528,7 @@
     1.4    by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
     1.5      \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
     1.6  
     1.7 -interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
     1.8 +interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<subseteq>#" "op \<subset>#"
     1.9    by standard
    1.10      \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    1.11  
    1.12 @@ -547,7 +547,7 @@
    1.13     apply (auto intro: multiset_eq_iff [THEN iffD2])
    1.14    done
    1.15  
    1.16 -interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
    1.17 +interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<subseteq>#" "op \<subset>#" "op -"
    1.18    by standard (simp, fact mset_subset_eq_exists_conv)
    1.19      \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    1.20  
    1.21 @@ -628,8 +628,8 @@
    1.22  lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
    1.23    by (simp only: subset_mset.not_less_zero)
    1.24  
    1.25 -lemma empty_subset_add_mset[simp]: "{#} <# add_mset x M"
    1.26 -by(auto intro: subset_mset.gr_zeroI)
    1.27 +lemma empty_subset_add_mset[simp]: "{#} \<subset># add_mset x M"
    1.28 +  by (auto intro: subset_mset.gr_zeroI)
    1.29  
    1.30  lemma empty_le: "{#} \<subseteq># A"
    1.31    by (fact subset_mset.zero_le)