src/HOL/Lifting.thy
changeset 47521 69f95ac85c3d
parent 47501 0b9294e093db
child 47534 06cc372a80ed
     1.1 --- a/src/HOL/Lifting.thy	Tue Apr 17 16:14:07 2012 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Tue Apr 17 19:16:13 2012 +0200
     1.3 @@ -218,6 +218,10 @@
     1.4      done
     1.5  qed
     1.6  
     1.7 +lemma equivp_reflp2:
     1.8 +  "equivp R \<Longrightarrow> reflp R"
     1.9 +  by (erule equivpE)
    1.10 +
    1.11  subsection {* Invariant *}
    1.12  
    1.13  definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"