src/HOL/Cardinals/Wellorder_Relation_LFP.thy

--- a/src/HOL/Cardinals/Wellorder_Relation_LFP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation_LFP.thy	Mon Nov 18 18:04:45 2013 +0100
@@ -419,7 +419,7 @@
 qed
 
 
-subsubsection {* Properties of order filters  *}
+subsubsection {* Properties of order filters *}
 
 
 lemma under_ofilter:
@@ -513,44 +513,6 @@
 qed
 
 
-lemma ofilter_Under:
-assumes "A \<le> Field r"
-shows "ofilter(Under A)"
-proof(unfold ofilter_def, auto)
-  fix x assume "x \<in> Under A"
-  thus "x \<in> Field r"
-  using Under_Field assms by auto
-next
-  fix a x
-  assume "a \<in> Under A" and "x \<in> under a"
-  thus "x \<in> Under A"
-  using TRANS under_Under_trans by auto
-qed
-
-
-lemma ofilter_UnderS:
-assumes "A \<le> Field r"
-shows "ofilter(UnderS A)"
-proof(unfold ofilter_def, auto)
-  fix x assume "x \<in> UnderS A"
-  thus "x \<in> Field r"
-  using UnderS_Field assms by auto
-next
-  fix a x
-  assume "a \<in> UnderS A" and "x \<in> under a"
-  thus "x \<in> UnderS A"
-  using TRANS ANTISYM under_UnderS_trans by auto
-qed
-
-
-lemma ofilter_Int: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)"
-unfolding ofilter_def by blast
-
-
-lemma ofilter_Un: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A \<union> B)"
-unfolding ofilter_def by blast
-
-
 lemma ofilter_UNION:
 "(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
 unfolding ofilter_def by blast