# HG changeset patch
# User haftmann
# Date 1427367632 -3600
# Node ID 75433c3ee2036d7a02608ace29c266acbbe3a55f
# Parent  034b13f4efae78f50f44d89a857b477f1e2fc7b4
restored broken metis proof

diff -r 034b13f4efae -r 75433c3ee203 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Thu Mar 26 12:00:32 2015 +0100
@@ -299,8 +299,8 @@
 
 lemma ex_gt_count_imp_less_multiset:
   "(\<forall>y \<Colon> 'a \<Colon> linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M \<subset># N"
-  unfolding less_multiset\<^sub>H\<^sub>O by (metis UnCI comm_monoid_diff_class.diff_cancel dual_order.asym
-    less_imp_diff_less mem_set_of_iff order.not_eq_order_implies_strict set_of_union)
+  unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order
+    less_not_sym mset_leD mset_le_add_left)  
 
 lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N \<subset># P \<Longrightarrow> M - P + N \<subset># M"
   by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2)