author | huffman |
Mon, 14 May 2012 17:09:11 +0200 | |
changeset 47922 | bba52dffab2b |
parent 47921 | fc26d5538868 |
child 47923 | ba9df9685e7c |
--- 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]: