src/HOL/Library/Multiset.thy
changeset 55565 f663fc1e653b
parent 55467 a5c9002bc54d
child 55808 488c3e8282c8
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Feb 18 23:03:49 2014 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Feb 18 23:03:50 2014 +0100
     1.3 @@ -268,8 +268,8 @@
     1.4  instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
     1.5  begin
     1.6  
     1.7 -lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)"
     1.8 -by simp
     1.9 +lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)" .
    1.10 +
    1.11  lemmas mset_le_def = less_eq_multiset_def
    1.12  
    1.13  definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where