# HG changeset patch
# User huffman
# Date 1337008151 -7200
# Node ID bba52dffab2bd165b1e68726d1c0c5ceee27b0cf
# Parent  fc26d5538868d6a098ebc3839422d9388cffc30c
add transfer rule for set_rel

diff -r fc26d5538868 -r bba52dffab2b src/HOL/Library/Quotient_Set.thy
--- 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]: