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