# HG changeset patch
# User traytel
# Date 1391081262 -3600
# Node ID 5556470a02b703de06aefd841631c276eb7a2974
# Parent  dc7a6f6be01bc2435a1223d0de0fa1c15931f034
define ofilter outside of wo_rel

diff -r dc7a6f6be01b -r 5556470a02b7 src/HOL/BNF_Wellorder_Relation.thy
--- a/src/HOL/BNF_Wellorder_Relation.thy	Thu Jan 30 01:03:55 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Relation.thy	Thu Jan 30 12:27:42 2014 +0100
@@ -34,6 +34,8 @@
 abbreviation aboveS where "aboveS \<equiv> Order_Relation.aboveS r"
 abbreviation Above where "Above \<equiv> Order_Relation.Above r"
 abbreviation AboveS where "AboveS \<equiv> Order_Relation.AboveS r"
+abbreviation ofilter where "ofilter \<equiv> Order_Relation.ofilter r"
+lemmas ofilter_def = Order_Relation.ofilter_def[of r]
 
 
 subsection {* Auxiliaries *}
@@ -139,10 +141,6 @@
 definition suc :: "'a set \<Rightarrow> 'a"
 where "suc A \<equiv> minim (AboveS A)"
 
-definition ofilter :: "'a set \<Rightarrow> bool"
-where
-"ofilter A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under a \<le> A)"
-
 
 subsubsection {* Properties of max2 *}
 
@@ -438,7 +436,7 @@
     hence 2: "?a \<in> Field r" using minim_inField[of ?B] by blast
     have 3: "?a \<in> ?B" using minim_in[of ?B] 1 by blast
     hence 4: "?a \<notin> A" by blast
-    have 5: "A \<le> Field r" using * ofilter_def[of A] by auto
+    have 5: "A \<le> Field r" using * ofilter_def by auto
     (*  *)
     moreover
     have "A = underS ?a"
diff -r dc7a6f6be01b -r 5556470a02b7 src/HOL/Cardinals/Wellorder_Relation.thy
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Jan 30 01:03:55 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Jan 30 12:27:42 2014 +0100
@@ -530,6 +530,5 @@
 abbreviation "max2 \<equiv> wo_rel.max2"
 abbreviation "supr \<equiv> wo_rel.supr"
 abbreviation "suc \<equiv> wo_rel.suc"
-abbreviation "ofilter \<equiv> wo_rel.ofilter"
 
 end
diff -r dc7a6f6be01b -r 5556470a02b7 src/HOL/Order_Relation.thy
--- 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. *}