changeset 47922 | bba52dffab2b |
parent 47777 | f29e7dcd7c40 |
child 47936 | 756f30eac792 |
--- a/src/HOL/Library/Quotient_Set.thy Mon May 14 15:54:26 2012 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Mon May 14 17:09:11 2012 +0200 @@ -112,6 +112,11 @@ apply (simp add: set_rel_def, fast) done +lemma set_rel_transfer [transfer_rule]: + "((A ===> B ===> op =) ===> set_rel A ===> set_rel B ===> op =) + set_rel set_rel" + unfolding fun_rel_def set_rel_def by fast + subsubsection {* Rules requiring bi-unique or bi-total relations *} lemma member_transfer [transfer_rule]: