src/HOL/BNF/BNF_GFP.thy

--- a/src/HOL/BNF/BNF_GFP.thy	Tue Aug 20 16:10:58 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Tue Aug 20 17:39:07 2013 +0200
@@ -70,9 +70,6 @@
 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
 unfolding image2_def by auto
 
-lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
-by auto
-
 lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
 by auto