--- a/src/HOL/Order_Relation.thy Thu Jan 30 01:03:55 2014 +0100
+++ b/src/HOL/Order_Relation.thy Thu Jan 30 12:27:42 2014 +0100
@@ -210,6 +210,9 @@
definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
+definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
+where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)"
+
text{* Note: In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
we bounded comprehension by @{text "Field r"} in order to properly cover
the case of @{text "A"} being empty. *}