--- a/src/HOL/Library/Multiset.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Feb 18 23:03:50 2014 +0100
@@ -268,8 +268,8 @@
instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
begin
-lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)"
-by simp
+lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)" .
+
lemmas mset_le_def = less_eq_multiset_def
definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where