src/HOL/Library/Multiset.thy

    apply (auto intro: multiset_eq_iff [THEN iffD2])
   done
 
 interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
   by standard (simp, fact mset_subset_eq_exists_conv)
+
+declare subset_mset.add_diff_assoc[simp] subset_mset.add_diff_assoc2[simp]
 
 lemma mset_subset_eq_mono_add_right_cancel: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
    by (fact subset_mset.add_le_cancel_right)
 
 lemma mset_subset_eq_mono_add_left_cancel: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"

     case True
     moreover have "\<exists>j\<in>#J. (k, j) \<in> r" if "k \<in># K'" for k
       using K N trans True by (meson that transE)
     ultimately show ?thesis
       by (rule_tac x = I in exI, rule_tac x = J in exI, rule_tac x = "(K - {#a#}) + K'" in exI)
-        (use z y N in \<open>auto simp: subset_mset.add_diff_assoc dest: in_diffD\<close>)
+        (use z y N in \<open>auto simp del: subset_mset.add_diff_assoc2 dest: in_diffD\<close>)
   next
     case False
     then have "a \<in># I" by (metis N(2) union_iff union_single_eq_member z)
     moreover have "M0 = I + K - {#a#}"
       using N(2) z by force
     ultimately show ?thesis
       by (rule_tac x = "I - {#a#}" in exI, rule_tac x = "add_mset a J" in exI,
           rule_tac x = "K + K'" in exI)
-        (use z y N False K in \<open>auto simp: subset_mset.diff_add_assoc2\<close>)
+        (use z y N False K in \<open>auto simp: add.assoc\<close>)
   qed
 qed
 
 lemma one_step_implies_mult:
   assumes