src/HOL/Lifting.thy
changeset 55083 0a689157e3ce
parent 53952 b2781a3ce958
child 55563 a64d49f49ca3
     1.1 --- a/src/HOL/Lifting.thy	Mon Jan 20 20:00:33 2014 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Mon Jan 20 20:21:12 2014 +0100
     1.3 @@ -484,9 +484,6 @@
     1.4  
     1.5  text {* Proving a parametrized correspondence relation *}
     1.6  
     1.7 -lemma eq_OO: "op= OO R = R"
     1.8 -unfolding OO_def by metis
     1.9 -
    1.10  definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
    1.11  "POS A B \<equiv> A \<le> B"
    1.12