src/HOL/Library/Quotient_Set.thy
changeset 47936 756f30eac792
parent 47922 bba52dffab2b
child 47982 7aa35601ff65
--- a/src/HOL/Library/Quotient_Set.thy	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Wed May 16 19:15:45 2012 +0200
@@ -34,7 +34,7 @@
 lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
   unfolding set_rel_def fun_eq_iff by auto
 
-lemma reflp_set_rel: "reflp R \<Longrightarrow> reflp (set_rel R)"
+lemma reflp_set_rel[reflp_preserve]: "reflp R \<Longrightarrow> reflp (set_rel R)"
   unfolding reflp_def set_rel_def by fast
 
 lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"