1.1 --- a/src/HOL/Library/Quotient_Set.thy	Sun Apr 22 19:44:40 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Sun Apr 22 20:16:30 2012 +0200
     1.3 @@ -129,6 +129,13 @@
     1.4    shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter"
     1.5    using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
     1.6  
     1.7 +lemma Diff_transfer [transfer_rule]:
     1.8 +  assumes "bi_unique A"
     1.9 +  shows "(set_rel A ===> set_rel A ===> set_rel A) (op -) (op -)"
    1.10 +  using assms unfolding fun_rel_def set_rel_def bi_unique_def
    1.11 +  unfolding Ball_def Bex_def Diff_eq
    1.12 +  by (safe, simp, metis, simp, metis)
    1.13 +
    1.14  lemma subset_transfer [transfer_rule]:
    1.15    assumes [transfer_rule]: "bi_unique A"
    1.16    shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)"