diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -305,6 +305,9 @@
 interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" 0 "op \<le>#" "op <#" "op -"
   by standard (simp, fact mset_le_exists_conv)
 
+declare subset_mset.zero_order[simp del]
+  -- \<open>this removes some simp rules not in the usual order for multisets\<close>
+
 lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B"
   by (fact subset_mset.add_le_cancel_right)
 
@@ -382,7 +385,7 @@
   by (fact subset_mset.add_less_imp_less_right)
 
 lemma mset_less_empty_nonempty: "{#} <# S \<longleftrightarrow> S \<noteq> {#}"
-  by (auto simp: subset_mset_def subseteq_mset_def)
+  by (fact subset_mset.zero_less_iff_neq_zero)
 
 lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} <# B"
   by (auto simp: subset_mset_def subseteq_mset_def multiset_eq_iff)