src/HOL/Library/Multiset.thy
changeset 55945 e96383acecf9
parent 55913 c1409c103b77
child 56656 7f9b686bf30a
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Mar 06 15:29:18 2014 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Mar 06 15:40:33 2014 +0100
     1.3 @@ -2289,7 +2289,7 @@
     1.4  interpretation lifting_syntax .
     1.5  
     1.6  lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of"
     1.7 -  unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
     1.8 +  unfolding set_of_def pcr_multiset_def cr_multiset_def rel_fun_def by auto
     1.9  
    1.10  end
    1.11