--- a/src/HOL/Lifting.thy Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Lifting.thy Wed May 16 19:15:45 2012 +0200
@@ -100,6 +100,9 @@
lemma identity_quotient: "Quotient (op =) id id (op =)"
unfolding Quotient_def by simp
+lemma reflp_equality: "reflp (op =)"
+by (auto intro: reflpI)
+
text {* TODO: Use one of these alternatives as the real definition. *}
lemma Quotient_alt_def:
@@ -364,6 +367,7 @@
setup Lifting_Info.setup
declare fun_quotient[quot_map]
+declare reflp_equality[reflp_preserve]
use "Tools/Lifting/lifting_term.ML"