src/HOL/Lifting.thy
changeset 59726 64c2bb331035
parent 58889 5b7a9633cfa8
child 60229 4cd6462c1fda
     1.1 --- a/src/HOL/Lifting.thy	Mon Mar 16 23:00:38 2015 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Mon Mar 16 23:05:56 2015 +0100
     1.3 @@ -376,9 +376,6 @@
     1.4  lemma reflp_ge_eq:
     1.5    "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast
     1.6  
     1.7 -lemma ge_eq_refl:
     1.8 -  "R \<ge> op= \<Longrightarrow> R x x" by blast
     1.9 -
    1.10  text {* Proving a parametrized correspondence relation *}
    1.11  
    1.12  definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where