1.1 --- a/src/HOL/Library/Quotient_Set.thy	Fri Mar 23 14:18:43 2012 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Fri Mar 23 14:20:09 2012 +0100
     1.3 @@ -26,6 +26,8 @@
     1.4      by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
     1.5  qed
     1.6  
     1.7 +declare [[map set = (set_rel, set_quotient)]]
     1.8 +
     1.9  lemma empty_set_rsp[quot_respect]:
    1.10    "set_rel R {} {}"
    1.11    unfolding set_rel_def by simp