--- a/src/HOL/Library/Quotient_Set.thy Sat Apr 21 21:38:08 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Sun Apr 22 11:05:04 2012 +0200
@@ -91,6 +91,10 @@
"((A ===> B) ===> set_rel A ===> set_rel B) image image"
unfolding fun_rel_def set_rel_def by simp fast
+lemma UNION_transfer [transfer_rule]:
+ "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) UNION UNION"
+ unfolding SUP_def [abs_def] by transfer_prover
+
lemma Ball_transfer [transfer_rule]:
"(set_rel A ===> (A ===> op =) ===> op =) Ball Ball"
unfolding set_rel_def fun_rel_def by fast