--- a/src/HOL/Library/Quotient_Set.thy Sun Apr 22 19:44:40 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Sun Apr 22 20:16:30 2012 +0200
@@ -129,6 +129,13 @@
shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter"
using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
+lemma Diff_transfer [transfer_rule]:
+ assumes "bi_unique A"
+ shows "(set_rel A ===> set_rel A ===> set_rel A) (op -) (op -)"
+ using assms unfolding fun_rel_def set_rel_def bi_unique_def
+ unfolding Ball_def Bex_def Diff_eq
+ by (safe, simp, metis, simp, metis)
+
lemma subset_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)"