src/HOL/Lifting.thy
changeset 47936 756f30eac792
parent 47889 29212a4bb866
child 47937 70375fa2679d
     1.1 --- a/src/HOL/Lifting.thy	Wed May 16 18:16:51 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed May 16 19:15:45 2012 +0200
     1.3 @@ -100,6 +100,9 @@
     1.4  lemma identity_quotient: "Quotient (op =) id id (op =)"
     1.5  unfolding Quotient_def by simp 
     1.6  
     1.7 +lemma reflp_equality: "reflp (op =)"
     1.8 +by (auto intro: reflpI)
     1.9 +
    1.10  text {* TODO: Use one of these alternatives as the real definition. *}
    1.11  
    1.12  lemma Quotient_alt_def:
    1.13 @@ -364,6 +367,7 @@
    1.14  setup Lifting_Info.setup
    1.15  
    1.16  declare fun_quotient[quot_map]
    1.17 +declare reflp_equality[reflp_preserve]
    1.18  
    1.19  use "Tools/Lifting/lifting_term.ML"
    1.20