# HG changeset patch
# User blanchet
# Date 1389901974 -3600
# Node ID 38db7814481d745f0d4d8fe82da57cd6eaf7a187
# Parent  eeba3ba734869e2f915dc6721602284c194efb85
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'

diff -r eeba3ba73486 -r 38db7814481d src/HOL/BNF/BNF_LFP.thy
--- a/src/HOL/BNF/BNF_LFP.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/BNF/BNF_LFP.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -30,14 +30,14 @@
 lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
 by auto
 
-lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> rel.underS R j"
-unfolding rel.underS_def by simp
+lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j"
+unfolding underS_def by simp
 
-lemma underS_E: "i \<in> rel.underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
-unfolding rel.underS_def by simp
+lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
+unfolding underS_def by simp
 
-lemma underS_Field: "i \<in> rel.underS R j \<Longrightarrow> i \<in> Field R"
-unfolding rel.underS_def Field_def by auto
+lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
+unfolding underS_def Field_def by auto
 
 lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
 unfolding Field_def by auto
diff -r eeba3ba73486 -r 38db7814481d src/HOL/BNF/Tools/bnf_lfp_util.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_util.ML	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_util.ML	Thu Jan 16 20:52:54 2014 +0100
@@ -34,7 +34,7 @@
 
 fun mk_underS r =
   let val T = fst (dest_relT (fastype_of r));
-  in Const (@{const_name rel.underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end;
+  in Const (@{const_name underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end;
 
 fun mk_worec r f =
   let val (A, AB) = apfst domain_type (dest_funT (fastype_of f));
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -1012,11 +1012,11 @@
 
 lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
 by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
-   simp add: Field_natLeq, unfold rel.under_def, auto)
+   simp add: Field_natLeq, unfold under_def, auto)
 
 lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
 by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
-   simp add: Field_natLeq, unfold rel.under_def, auto)
+   simp add: Field_natLeq, unfold under_def, auto)
 
 lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
 using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
@@ -1047,7 +1047,7 @@
 proof(rule iffI)
   assume "ofilter natLeq A"
   hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
-  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def rel.under_def)
+  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def under_def)
   thus "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
 next
   assume "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
@@ -1056,22 +1056,22 @@
 qed
 
 lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
-unfolding rel.under_def by auto
+unfolding under_def by auto
 
 lemma natLeq_on_ofilter_less_eq:
 "n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
 apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
 apply (simp add: Field_natLeq_on)
-by (auto simp add: rel.under_def)
+by (auto simp add: under_def)
 
 lemma natLeq_on_ofilter_iff:
 "wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
 proof(rule iffI)
   assume *: "wo_rel.ofilter (natLeq_on m) A"
   hence 1: "A \<le> {0..<m}"
-  by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on)
+  by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def Field_natLeq_on)
   hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
-  using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def)
+  using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def)
   hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
   thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
 next
@@ -1086,7 +1086,7 @@
 lemma natLeq_on_ofilter_less:
 "n < m \<Longrightarrow> ofilter (natLeq_on m) {0 .. n}"
 by(auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def,
-   simp add: Field_natLeq_on, unfold rel.under_def, auto)
+   simp add: Field_natLeq_on, unfold under_def, auto)
 
 lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
 using Field_natLeq Field_natLeq_on[of n]
@@ -1331,13 +1331,13 @@
 lemma under_mono[simp]:
 assumes "Well_order r" and "(i,j) \<in> r"
 shows "under r i \<subseteq> under r j"
-using assms unfolding rel.under_def order_on_defs
+using assms unfolding under_def order_on_defs
 trans_def by blast
 
 lemma underS_under:
 assumes "i \<in> Field r"
 shows "underS r i = under r i - {i}"
-using assms unfolding rel.underS_def rel.under_def by auto
+using assms unfolding underS_def under_def by auto
 
 lemma relChain_under:
 assumes "Well_order r"
@@ -1593,7 +1593,7 @@
     unfolding p_def apply(rule Refl_Field_Restr2[OF rr]) by auto
     have of: "ofilter r (Field p)" unfolding wo_rel.ofilter_def[OF 0] proof safe
       fix a x assume a: "a \<in> Field p" and "x \<in> under r a"
-      hence x: "(x,a) \<in> r" "x \<in> Field r" unfolding rel.under_def Field_def by auto
+      hence x: "(x,a) \<in> r" "x \<in> Field r" unfolding under_def Field_def by auto
       moreover have a: "a \<noteq> j" "a \<in> Field r" "(a,j) \<in> r" using a jm  unfolding fp by auto
       ultimately have "x \<noteq> j" using j jm  by (metis 0 wo_rel.max2_def wo_rel.max2_equals1)
       thus "x \<in> Field p" using x unfolding fp by auto
@@ -1654,7 +1654,7 @@
     hence "As (succ r i) \<subseteq> As j" using rc unfolding relChain_def by auto
     moreover
     {have "(i,succ r i) \<in> r" apply(rule wo_rel.succ_in[OF 0])
-     using 1 unfolding rel.aboveS_def by auto
+     using 1 unfolding aboveS_def by auto
      hence "As i \<subset> As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto
     }
     ultimately show False unfolding Asij by auto
@@ -1721,13 +1721,13 @@
    def g \<equiv> "\<lambda> a. if F a \<noteq> {} then gg a else j0"
    have g: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u),g a) \<in> r" using gg unfolding g_def by auto
    hence 1: "Field r \<subseteq> (\<Union> a \<in> A. under r (g a))"
-   using f[symmetric] unfolding rel.under_def image_def by auto
+   using f[symmetric] unfolding under_def image_def by auto
    have gA: "g ` A \<subseteq> Field r" using gg j0 unfolding Field_def g_def by auto
    moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe
      fix i assume "i \<in> Field r"
      then obtain j where ij: "(i,j) \<in> r" "i \<noteq> j" using cr ir by (metis infinite_Card_order_limit)
-     hence "j \<in> Field r" by (metis card_order_on_def cr rel.well_order_on_domain)
-     then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding rel.under_def by auto
+     hence "j \<in> Field r" by (metis card_order_on_def cr well_order_on_domain)
+     then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding under_def by auto
      hence "(i, g a) \<in> r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast
      moreover have "i \<noteq> g a"
      using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def
@@ -1752,7 +1752,7 @@
   {assume Kr: "|K| <o r"
    then obtain f where "\<forall> a \<in> Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r"
    using cof unfolding cofinal_def by metis
-   hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding rel.underS_def by auto
+   hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding underS_def by auto
    hence "r \<le>o |\<Union> a \<in> K. underS r a|" using cr
    by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive)
    also have "|\<Union> a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -59,7 +59,7 @@
 
 lemma card_order_on_Card_order:
 "card_order_on A r \<Longrightarrow> A = Field r \<and> Card_order r"
-unfolding card_order_on_def using rel.well_order_on_Field by blast
+unfolding card_order_on_def using well_order_on_Field by blast
 
 
 text{* The existence of a cardinal relation on any given set (which will mean
@@ -77,7 +77,7 @@
 proof-
   obtain R where R_def: "R = {r. well_order_on A r}" by blast
   have 1: "R \<noteq> {} \<and> (\<forall>r \<in> R. Well_order r)"
-  using well_order_on[of A] R_def rel.well_order_on_Well_order by blast
+  using well_order_on[of A] R_def well_order_on_Well_order by blast
   hence "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
   using  exists_minim_Well_order[of R] by auto
   thus ?thesis using R_def unfolding card_order_on_def by auto
@@ -98,7 +98,7 @@
 proof(unfold card_order_on_def, auto)
   fix p' assume "well_order_on (Field r') p'"
   hence 0: "Well_order p' \<and> Field p' = Field r'"
-  using rel.well_order_on_Well_order by blast
+  using well_order_on_Well_order by blast
   obtain f where 1: "iso r' r f" and 2: "Well_order r \<and> Well_order r'"
   using ISO unfolding ordIso_def by auto
   hence 3: "inj_on f (Field r') \<and> f ` (Field r') = Field r"
@@ -143,7 +143,7 @@
 
 lemma Field_card_of: "Field |A| = A"
 using card_of_card_order_on[of A] unfolding card_order_on_def
-using rel.well_order_on_Field by blast
+using well_order_on_Field by blast
 
 
 lemma card_of_Card_order: "Card_order |A|"
@@ -273,7 +273,7 @@
   obtain f where
   1: "well_order_on (Field r) r \<and> well_order_on (Field r) r \<and> embed r r' f"
   using assms unfolding ordLeq_def
-  by (auto simp add: rel.well_order_on_Well_order)
+  by (auto simp add: well_order_on_Well_order)
   hence "inj_on f (Field r) \<and> f ` (Field r) \<le> Field r'"
   by (auto simp add: embed_inj_on embed_Field)
   thus "|Field r| \<le>o |Field r'|" using card_of_ordLeq by blast
@@ -285,7 +285,7 @@
 
 
 lemma card_of_Field_ordLess: "Well_order r \<Longrightarrow> |Field r| \<le>o r"
-using card_of_least card_of_well_order_on rel.well_order_on_Well_order by blast
+using card_of_least card_of_well_order_on well_order_on_Well_order by blast
 
 
 lemma card_of_Field_ordIso:
@@ -321,16 +321,16 @@
 
 lemma Card_order_iff_Restr_underS:
 assumes "Well_order r"
-shows "Card_order r = (\<forall>a \<in> Field r. Restr r (rel.underS r a) <o |Field r| )"
+shows "Card_order r = (\<forall>a \<in> Field r. Restr r (underS r a) <o |Field r| )"
 using assms unfolding Card_order_iff_ordLeq_card_of
 using ordLeq_iff_ordLess_Restr card_of_Well_order by blast
 
 
 lemma card_of_underS:
 assumes r: "Card_order r" and a: "a : Field r"
-shows "|rel.underS r a| <o r"
+shows "|underS r a| <o r"
 proof-
-  let ?A = "rel.underS r a"  let ?r' = "Restr r ?A"
+  let ?A = "underS r a"  let ?r' = "Restr r ?A"
   have 1: "Well_order r"
   using r unfolding card_order_on_def by simp
   have "Well_order ?r'" using 1 Well_order_Restr by auto
@@ -355,7 +355,7 @@
 shows "|Field r| <o r'"
 proof-
   have "well_order_on (Field r) r" using assms unfolding ordLess_def
-  by (auto simp add: rel.well_order_on_Well_order)
+  by (auto simp add: well_order_on_Well_order)
   hence "|Field r| \<le>o r" using card_of_least by blast
   thus ?thesis using assms ordLeq_ordLess_trans by blast
 qed
@@ -937,35 +937,35 @@
 
 lemma Card_order_infinite_not_under:
 assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
-shows "\<not> (\<exists>a. Field r = rel.under r a)"
+shows "\<not> (\<exists>a. Field r = under r a)"
 proof(auto)
   have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
   using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto
-  fix a assume *: "Field r = rel.under r a"
+  fix a assume *: "Field r = under r a"
   show False
   proof(cases "a \<in> Field r")
     assume Case1: "a \<notin> Field r"
-    hence "rel.under r a = {}" unfolding Field_def rel.under_def by auto
+    hence "under r a = {}" unfolding Field_def under_def by auto
     thus False using INF *  by auto
   next
-    let ?r' = "Restr r (rel.underS r a)"
+    let ?r' = "Restr r (underS r a)"
     assume Case2: "a \<in> Field r"
-    hence 1: "rel.under r a = rel.underS r a \<union> {a} \<and> a \<notin> rel.underS r a"
-    using 0 rel.Refl_under_underS rel.underS_notIn by metis
-    have 2: "wo_rel.ofilter r (rel.underS r a) \<and> rel.underS r a < Field r"
+    hence 1: "under r a = underS r a \<union> {a} \<and> a \<notin> underS r a"
+    using 0 Refl_under_underS underS_notIn by metis
+    have 2: "wo_rel.ofilter r (underS r a) \<and> underS r a < Field r"
     using 0 wo_rel.underS_ofilter * 1 Case2 by fast
     hence "?r' <o r" using 0 using ofilter_ordLess by blast
     moreover
-    have "Field ?r' = rel.underS r a \<and> Well_order ?r'"
+    have "Field ?r' = underS r a \<and> Well_order ?r'"
     using  2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast
-    ultimately have "|rel.underS r a| <o r" using ordLess_Field[of ?r'] by auto
-    moreover have "|rel.under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
-    ultimately have "|rel.underS r a| <o |rel.under r a|"
+    ultimately have "|underS r a| <o r" using ordLess_Field[of ?r'] by auto
+    moreover have "|under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
+    ultimately have "|underS r a| <o |under r a|"
     using ordIso_symmetric ordLess_ordIso_trans by blast
     moreover
-    {have "\<exists>f. bij_betw f (rel.under r a) (rel.underS r a)"
+    {have "\<exists>f. bij_betw f (under r a) (underS r a)"
      using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto
-     hence "|rel.under r a| =o |rel.underS r a|" using card_of_ordIso by blast
+     hence "|under r a| =o |underS r a|" using card_of_ordIso by blast
     }
     ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast
   qed
@@ -977,13 +977,13 @@
 and a: "a : Field r"
 shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
 proof-
-  have "Field r \<noteq> rel.under r a"
+  have "Field r \<noteq> under r a"
   using assms Card_order_infinite_not_under by blast
-  moreover have "rel.under r a \<le> Field r"
-  using rel.under_Field .
-  ultimately have "rel.under r a < Field r" by blast
+  moreover have "under r a \<le> Field r"
+  using under_Field .
+  ultimately have "under r a < Field r" by blast
   then obtain b where 1: "b : Field r \<and> ~ (b,a) : r"
-  unfolding rel.under_def by blast
+  unfolding under_def by blast
   moreover have ba: "b \<noteq> a"
   using 1 r unfolding card_order_on_def well_order_on_def
   linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto
@@ -1036,7 +1036,7 @@
     using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto
     hence temp2: "wo_rel.ofilter ?r' ?B \<and> ?B < ?A \<times> ?A"
     using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast
-    have "\<not> (\<exists>a. Field r = rel.under r a)"
+    have "\<not> (\<exists>a. Field r = under r a)"
     using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto
     then obtain A1 where temp3: "wo_rel.ofilter r A1 \<and> A1 < ?A" and 9: "?B \<le> A1 \<times> A1"
     using temp2 3 bsqr_ofilter[of r ?B] by blast
@@ -1332,8 +1332,8 @@
 unfolding Field_def by auto
 
 
-lemma natLeq_underS_less: "rel.underS natLeq n = {x. x < n}"
-unfolding rel.underS_def by auto
+lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"
+unfolding underS_def by auto
 
 
 lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
@@ -1341,7 +1341,7 @@
 
 
 lemma Restr_natLeq2:
-"Restr natLeq (rel.underS natLeq n) = natLeq_on n"
+"Restr natLeq (underS natLeq n) = natLeq_on n"
 by (auto simp add: Restr_natLeq natLeq_underS_less)
 
 
@@ -1728,7 +1728,7 @@
     using r' by (simp add: card_of_Field_ordIso[of ?r'])
     finally have "|K| \<le>o ?r'" .
     moreover
-    {let ?L = "UN j : K. rel.underS ?r' j"
+    {let ?L = "UN j : K. underS ?r' j"
      let ?J = "Field r"
      have rJ: "r =o |?J|"
      using r_card card_of_Field_ordIso ordIso_symmetric by blast
@@ -1736,11 +1736,11 @@
      hence "|K| <=o r" using r' card_of_Card_order[of K] by blast
      hence "|K| \<le>o |?J|" using rJ ordLeq_ordIso_trans by blast
      moreover
-     {have "ALL j : K. |rel.underS ?r' j| <o ?r'"
+     {have "ALL j : K. |underS ?r' j| <o ?r'"
       using r' 1 by (auto simp: card_of_underS)
-      hence "ALL j : K. |rel.underS ?r' j| \<le>o r"
+      hence "ALL j : K. |underS ?r' j| \<le>o r"
       using r' card_of_Card_order by blast
-      hence "ALL j : K. |rel.underS ?r' j| \<le>o |?J|"
+      hence "ALL j : K. |underS ?r' j| \<le>o |?J|"
       using rJ ordLeq_ordIso_trans by blast
      }
      ultimately have "|?L| \<le>o |?J|"
@@ -1750,7 +1750,7 @@
      moreover
      {
       have "Field ?r' \<le> ?L"
-      using 2 unfolding rel.underS_def cofinal_def by auto
+      using 2 unfolding underS_def cofinal_def by auto
       hence "|Field ?r'| \<le>o |?L|" by (simp add: card_of_mono1)
       hence "?r' \<le>o |?L|"
       using 22 ordIso_ordLeq_trans ordIso_symmetric by blast
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Constructions_on_Wellorders.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -216,7 +216,7 @@
   moreover
   have "ofilter (r Osum r') (Field r)"
   using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def
-                               Field_Osum rel.under_def)
+                               Field_Osum under_def)
     fix a b assume 2: "a \<in> Field r" and 3: "(b,a) \<in> r Osum r'"
     moreover
     {assume "(b,a) \<in> r'"
@@ -251,13 +251,13 @@
   then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''"
   using WELL  Well_order_iso_copy by blast
   hence 2: "Well_order r'' \<and> Field r'' = (f ` A)"
-  using rel.well_order_on_Well_order by blast
+  using well_order_on_Well_order by blast
   (*  *)
   let ?C = "B - (f ` A)"
   obtain r''' where "well_order_on ?C r'''"
   using well_order_on by blast
   hence 3: "Well_order r''' \<and> Field r''' = ?C"
-  using rel.well_order_on_Well_order by blast
+  using well_order_on_Well_order by blast
   (*  *)
   let ?r' = "r'' Osum r'''"
   have "Field r'' Int Field r''' = {}"
@@ -479,23 +479,18 @@
   have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
   assume "\<forall>a\<in>A.  b \<notin> under a"
   hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA unfolding underS_def
-  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq rel.under_def set_rev_mp)
-  have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding rel.underS_def by auto
+  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def set_rev_mp)
+  have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto
   thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
 qed
 
-lemma (in rel) AboveS_underS:
-assumes "i \<in> Field r"
-shows "i \<in> AboveS (underS i)"
-using assms unfolding AboveS_def underS_def by auto
-
 lemma (in wo_rel) in_underS_supr:
 assumes j: "j \<in> underS i" and i: "i \<in> A" and A: "A \<subseteq> Field r" and AA: "Above A \<noteq> {}"
 shows "j \<in> underS (supr A)"
 proof-
   have "(i,supr A) \<in> r" using supr_greater[OF A AA i] .
   thus ?thesis using j unfolding underS_def
-  by simp (metis REFL TRANS max2_def max2_equals1 rel.refl_on_domain transD)
+  by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD)
 qed
 
 lemma inj_on_Field:
@@ -530,7 +525,7 @@
   and init: "(R ja, R j) \<notin> init_seg_of"
   hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
   and jjai: "(j,i) \<in> r" "(ja,i) \<in> r"
-  and i: "i \<notin> {j,ja}" unfolding Field_def rel.underS_def by auto
+  and i: "i \<notin> {j,ja}" unfolding Field_def underS_def by auto
   have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
   show "R j initial_segment_of R ja"
   using jja init jjai i
@@ -544,7 +539,7 @@
   fix j ja assume jS: "j \<in> Field r" and jaS: "ja \<in> Field r"
   and init: "(R ja, R j) \<notin> init_seg_of"
   hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
-  unfolding Field_def rel.underS_def by auto
+  unfolding Field_def underS_def by auto
   have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
   show "R j initial_segment_of R ja"
   using jja init
@@ -700,8 +695,8 @@
 assumes "aboveS i \<noteq> {}"
 shows "(j, succ i) \<in> r \<longleftrightarrow> (j,i) \<in> r \<or> j = succ i"
 apply safe
-  apply (metis WELL assms in_notinI rel.well_order_on_domain suc_singl_pred succ_def succ_in_diff)
-  apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 rel.refl_on_domain succ_in_Field succ_not_in transD)
+  apply (metis WELL assms in_notinI well_order_on_domain suc_singl_pred succ_def succ_in_diff)
+  apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD)
   apply (metis assms in_notinI succ_in_Field)
 done
 
@@ -926,7 +921,7 @@
 lemma oproj_under: 
 assumes f:  "oproj r s f" and a: "a \<in> under r a'"
 shows "f a \<in> under s (f a')"
-using oproj_in[OF f] a unfolding rel.under_def by auto
+using oproj_in[OF f] a unfolding under_def by auto
 
 (* An ordinal is embedded in another whenever it is embedded as an order 
 (not necessarily as initial segment):*)
@@ -950,55 +945,55 @@
      and IH1a: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> inj_on g (under r a1)"
      and IH1b: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g ` under r a1 = under s (g a1)"
      and IH2: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> under s (f a1)"
-     unfolding rel.underS_def Field_def bij_betw_def by auto
+     unfolding underS_def Field_def bij_betw_def by auto
      have fa: "f a \<in> Field s" using f[OF a] by auto
      have g: "g a = suc s (g ` underS r a)" 
      using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by simp
      have A0: "g ` underS r a \<subseteq> Field s" 
-     using IH1b by (metis IH2 image_subsetI in_mono rel.under_Field)
+     using IH1b by (metis IH2 image_subsetI in_mono under_Field)
      {fix a1 assume a1: "a1 \<in> underS r a"
       from IH2[OF this] have "g a1 \<in> under s (f a1)" .
       moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto
-      ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS rel.under_underS_trans)
+      ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans)
      }
-     hence "f a \<in> AboveS s (g ` underS r a)" unfolding rel.AboveS_def 
-     using fa by simp (metis (lifting, full_types) mem_Collect_eq rel.underS_def)
+     hence "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def 
+     using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def)
      hence A: "AboveS s (g ` underS r a) \<noteq> {}" by auto
      have B: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (g a)"
      unfolding g apply(rule s.suc_underS[OF A0 A]) by auto
      {fix a1 a2 assume a2: "a2 \<in> underS r a" and 1: "a1 \<in> underS r a2"
       hence a12: "{a1,a2} \<subseteq> under r a2" and "a1 \<noteq> a2" using r.REFL a
-      unfolding rel.underS_def rel.under_def refl_on_def Field_def by auto 
+      unfolding underS_def under_def refl_on_def Field_def by auto 
       hence "g a1 \<noteq> g a2" using IH1a[OF a2] unfolding inj_on_def by auto
       hence "g a1 \<in> underS s (g a2)" using IH1b[OF a2] a12 
-      unfolding rel.underS_def rel.under_def by auto
+      unfolding underS_def under_def by auto
      } note C = this
      have ga: "g a \<in> Field s" unfolding g using s.suc_inField[OF A0 A] .
      have aa: "a \<in> under r a" 
-     using a r.REFL unfolding rel.under_def rel.underS_def refl_on_def by auto
+     using a r.REFL unfolding under_def underS_def refl_on_def by auto
      show ?case proof safe
        show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe
          show "inj_on g (under r a)" proof(rule r.inj_on_Field)
            fix a1 a2 assume "a1 \<in> under r a" and a2: "a2 \<in> under r a" and a1: "a1 \<in> underS r a2"
            hence a22: "a2 \<in> under r a2" and a12: "a1 \<in> under r a2" "a1 \<noteq> a2"
-           using a r.REFL unfolding rel.under_def rel.underS_def refl_on_def by auto
+           using a r.REFL unfolding under_def underS_def refl_on_def by auto
            show "g a1 \<noteq> g a2"
            proof(cases "a2 = a")
              case False hence "a2 \<in> underS r a" 
-             using a2 unfolding rel.underS_def rel.under_def by auto 
+             using a2 unfolding underS_def under_def by auto 
              from IH1a[OF this] show ?thesis using a12 a22 unfolding inj_on_def by auto
-           qed(insert B a1, unfold rel.underS_def, auto)
-         qed(unfold rel.under_def Field_def, auto)
+           qed(insert B a1, unfold underS_def, auto)
+         qed(unfold under_def Field_def, auto)
        next
          fix a1 assume a1: "a1 \<in> under r a" 
          show "g a1 \<in> under s (g a)"
          proof(cases "a1 = a")
            case True thus ?thesis 
-           using ga s.REFL unfolding refl_on_def rel.under_def by auto
+           using ga s.REFL unfolding refl_on_def under_def by auto
          next
            case False
-           hence a1: "a1 \<in> underS r a" using a1 unfolding rel.underS_def rel.under_def by auto 
-           thus ?thesis using B unfolding rel.underS_def rel.under_def by auto
+           hence a1: "a1 \<in> underS r a" using a1 unfolding underS_def under_def by auto 
+           thus ?thesis using B unfolding underS_def under_def by auto
          qed
        next
          fix b1 assume b1: "b1 \<in> under s (g a)"
@@ -1007,12 +1002,12 @@
            case True thus ?thesis using aa by auto
          next
            case False 
-           hence "b1 \<in> underS s (g a)" using b1 unfolding rel.underS_def rel.under_def by auto
+           hence "b1 \<in> underS s (g a)" using b1 unfolding underS_def under_def by auto
            from s.underS_suc[OF this[unfolded g] A0]
            obtain a1 where a1: "a1 \<in> underS r a" and b1: "b1 \<in> under s (g a1)" by auto
            obtain a2 where "a2 \<in> under r a1" and b1: "b1 = g a2" using IH1b[OF a1] b1 by auto
            hence "a2 \<in> under r a" using a1 
-           by (metis r.ANTISYM r.TRANS in_mono rel.underS_subset_under rel.under_underS_trans)
+           by (metis r.ANTISYM r.TRANS in_mono underS_subset_under under_underS_trans)
            thus ?thesis using b1 by auto
          qed
        qed
@@ -1022,9 +1017,9 @@
          then obtain a1 where a1: "b1 = g a1" and a1: "a1 \<in> underS r a" by auto
          hence "b1 \<in> underS s (f a)" 
          using a by (metis `\<And>a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (f a)`)
-         thus "f a \<noteq> b1 \<and> (b1, f a) \<in> s" unfolding rel.underS_def by auto
+         thus "f a \<noteq> b1 \<and> (b1, f a) \<in> s" unfolding underS_def by auto
        qed(insert fa, auto)
-       thus "g a \<in> under s (f a)" unfolding rel.under_def by auto
+       thus "g a \<in> under s (f a)" unfolding under_def by auto
      qed
    qed
   }
@@ -1046,7 +1041,7 @@
 theorem oproj_embed:
 assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
 shows "\<exists> g. embed s r g"
-proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold rel.underS_def, safe)
+proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe)
   fix b assume "b \<in> Field s"
   thus "inv_into (Field r) f b \<in> Field r" using oproj_Field2[OF f] by (metis imageI inv_into_into)
 next
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -116,12 +116,12 @@
 
 lemma ofilter_Restr_under:
 assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"
-shows "rel.under (Restr r A) a = rel.under r a"
+shows "under (Restr r A) a = under r a"
 using assms wo_rel_def
-proof(auto simp add: wo_rel.ofilter_def rel.under_def)
+proof(auto simp add: wo_rel.ofilter_def under_def)
   fix b assume *: "a \<in> A" and "(b,a) \<in> r"
-  hence "b \<in> rel.under r a \<and> a \<in> Field r"
-  unfolding rel.under_def using Field_def by fastforce
+  hence "b \<in> under r a \<and> a \<in> Field r"
+  unfolding under_def using Field_def by fastforce
   thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
 qed
 
@@ -137,7 +137,7 @@
     by (auto simp add: wo_rel_def wo_rel.ofilter_def)
   next
     fix a assume "a \<in> Field (Restr r A)"
-    thus "bij_betw id (rel.under (Restr r A) a) (rel.under r a)" using assms *
+    thus "bij_betw id (under (Restr r A) a) (under r a)" using assms *
     by (simp add: ofilter_Restr_under Field_Restr_ofilter)
   qed
 next
@@ -148,13 +148,13 @@
   {fix a assume "a \<in> A"
    hence "a \<in> Field(Restr r A)" using * assms
    by (simp add: order_on_defs Refl_Field_Restr2)
-   hence "bij_betw id (rel.under (Restr r A) a) (rel.under r a)"
+   hence "bij_betw id (under (Restr r A) a) (under r a)"
    using * unfolding embed_def by auto
-   hence "rel.under r a \<le> rel.under (Restr r A) a"
+   hence "under r a \<le> under (Restr r A) a"
    unfolding bij_betw_def by auto
-   also have "\<dots> \<le> Field(Restr r A)" by (simp add: rel.under_Field)
+   also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field)
    also have "\<dots> \<le> A" by (simp add: Field_Restr_subset)
-   finally have "rel.under r a \<le> A" .
+   finally have "under r a \<le> A" .
   }
   thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def)
 qed
@@ -173,13 +173,13 @@
   by (simp add: Well_order_Restr wo_rel_def)
   (* Main proof *)
   show ?thesis using WellB assms
-  proof(auto simp add: wo_rel.ofilter_def rel.under_def)
+  proof(auto simp add: wo_rel.ofilter_def under_def)
     fix a assume "a \<in> A" and *: "a \<in> B"
     hence "a \<in> Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def)
     with * show "a \<in> Field ?rB" using Field by auto
   next
     fix a b assume "a \<in> A" and "(b,a) \<in> r"
-    thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def rel.under_def)
+    thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def under_def)
   qed
 qed
 
@@ -312,12 +312,12 @@
     assume *: "wo_rel.ofilter r A" "A \<noteq> Field r" and
            **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B"
     then obtain a and b where 0: "a \<in> Field r \<and> b \<in> Field r" and
-                         1: "A = rel.underS r a \<and> B = rel.underS r b"
+                         1: "A = underS r a \<and> B = underS r b"
     using Well by (auto simp add: wo_rel.ofilter_underS_Field)
     hence "a \<noteq> b" using *** by auto
     moreover
     have "(a,b) \<in> r" using 0 1 Lo ***
-    by (auto simp add: rel.underS_incl_iff)
+    by (auto simp add: underS_incl_iff)
     moreover
     have "a = wo_rel.suc r A \<and> b = wo_rel.suc r B"
     using Well 0 1 by (simp add: wo_rel.suc_underS)
@@ -714,10 +714,10 @@
 
 corollary underS_Restr_ordLess:
 assumes "Well_order r" and "Field r \<noteq> {}"
-shows "Restr r (rel.underS r a) <o r"
+shows "Restr r (underS r a) <o r"
 proof-
-  have "rel.underS r a < Field r" using assms
-  by (simp add: rel.underS_Field3)
+  have "underS r a < Field r" using assms
+  by (simp add: underS_Field3)
   thus ?thesis using assms
   by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)
 qed
@@ -772,10 +772,10 @@
 
 lemma ordLess_iff_ordIso_Restr:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (rel.underS r a))"
+shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))"
 proof(auto)
-  fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (rel.underS r a)"
-  hence "Restr r (rel.underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
+  fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)"
+  hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
   thus "r' <o r" using ** ordIso_ordLess_trans by blast
 next
   assume "r' <o r"
@@ -783,7 +783,7 @@
                       2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r"
   unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast
   hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast
-  then obtain a where 3: "a \<in> Field r" and 4: "rel.underS r a = f ` (Field r')"
+  then obtain a where 3: "a \<in> Field r" and 4: "underS r a = f ` (Field r')"
   using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def)
   have "iso r' (Restr r (f ` (Field r'))) f"
   using embed_implies_iso_Restr 2 assms by blast
@@ -791,8 +791,8 @@
   using WELL Well_order_Restr by blast
   ultimately have "r' =o Restr r (f ` (Field r'))"
   using WELL' unfolding ordIso_def by auto
-  hence "r' =o Restr r (rel.underS r a)" using 4 by auto
-  thus "\<exists>a \<in> Field r. r' =o Restr r (rel.underS r a)" using 3 by auto
+  hence "r' =o Restr r (underS r a)" using 4 by auto
+  thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto
 qed
 
 
@@ -801,13 +801,13 @@
 proof
   assume *: "r' <o r"
   hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto
-  with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (rel.underS r a)"
+  with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (underS r a)"
   using ordLess_iff_ordIso_Restr by blast
-  let ?p = "Restr r (rel.underS r a)"
-  have "wo_rel.ofilter r (rel.underS r a)" using 0
+  let ?p = "Restr r (underS r a)"
+  have "wo_rel.ofilter r (underS r a)" using 0
   by (simp add: wo_rel_def wo_rel.underS_ofilter)
-  hence "Field ?p = rel.underS r a" using 0 Field_Restr_ofilter by blast
-  hence "Field ?p < Field r" using rel.underS_Field2 1 by fast
+  hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast
+  hence "Field ?p < Field r" using underS_Field2 1 by fast
   moreover have "?p <o r" using underS_Restr_ordLess[of r a] 0 1 by blast
   ultimately
   show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast
@@ -840,18 +840,18 @@
 
 lemma ordLeq_iff_ordLess_Restr:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (rel.underS r a) <o r')"
+shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')"
 proof(auto)
   assume *: "r \<le>o r'"
   fix a assume "a \<in> Field r"
-  hence "Restr r (rel.underS r a) <o r"
+  hence "Restr r (underS r a) <o r"
   using WELL underS_Restr_ordLess[of r] by blast
-  thus "Restr r (rel.underS r a) <o r'"
+  thus "Restr r (underS r a) <o r'"
   using * ordLess_ordLeq_trans by blast
 next
-  assume *: "\<forall>a \<in> Field r. Restr r (rel.underS r a) <o r'"
+  assume *: "\<forall>a \<in> Field r. Restr r (underS r a) <o r'"
   {assume "r' <o r"
-   then obtain a where "a \<in> Field r \<and> r' =o Restr r (rel.underS r a)"
+   then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)"
    using assms ordLess_iff_ordIso_Restr by blast
    hence False using * not_ordLess_ordIso ordIso_symmetric by blast
   }
@@ -879,14 +879,14 @@
 shows "r =o r'"
 proof-
   have 0: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
-  using assms rel.well_order_on_Well_order by blast
+  using assms well_order_on_Well_order by blast
   moreover
   have "\<forall>r r'. well_order_on A r \<and> well_order_on A r' \<and> r \<le>o r'
                   \<longrightarrow> r =o r'"
   proof(clarify)
     fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'"
     have 2: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
-    using * ** rel.well_order_on_Well_order by blast
+    using * ** well_order_on_Well_order by blast
     assume "r \<le>o r'"
     then obtain f where 1: "embed r r' f" and
                         "inj_on f A \<and> f ` A \<le> A"
@@ -1137,7 +1137,7 @@
 proof-
    let ?r' = "dir_image r f"
    have 1: "A = Field r \<and> Well_order r"
-   using WELL rel.well_order_on_Well_order by blast
+   using WELL well_order_on_Well_order by blast
    hence 2: "iso r ?r' f"
    using dir_image_iso using BIJ unfolding bij_betw_def by auto
    hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast
@@ -1576,7 +1576,7 @@
 lemma bsqr_ofilter:
 assumes WELL: "Well_order r" and
         OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and
-        NE: "\<not> (\<exists>a. Field r = rel.under r a)"
+        NE: "\<not> (\<exists>a. Field r = under r a)"
 shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A"
 proof-
   let ?r' = "bsqr r"
@@ -1587,17 +1587,17 @@
   (*  *)
   have "D < Field ?r'" unfolding Field_bsqr using SUB .
   with OF obtain a1 and a2 where
-  "(a1,a2) \<in> Field ?r'" and 1: "D = rel.underS ?r' (a1,a2)"
+  "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)"
   using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto
   hence 2: "{a1,a2} \<le> Field r" unfolding Field_bsqr by auto
   let ?m = "wo_rel.max2 r a1 a2"
-  have "D \<le> (rel.under r ?m) \<times> (rel.under r ?m)"
+  have "D \<le> (under r ?m) \<times> (under r ?m)"
   proof(unfold 1)
     {fix b1 b2
      let ?n = "wo_rel.max2 r b1 b2"
-     assume "(b1,b2) \<in> rel.underS ?r' (a1,a2)"
+     assume "(b1,b2) \<in> underS ?r' (a1,a2)"
      hence 3: "((b1,b2),(a1,a2)) \<in> ?r'"
-     unfolding rel.underS_def by blast
+     unfolding underS_def by blast
      hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2)
      moreover
      {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto
@@ -1607,13 +1607,13 @@
      }
      ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r"
      using Trans trans_def[of r] by blast
-     hence "(b1,b2) \<in> (rel.under r ?m) \<times> (rel.under r ?m)" unfolding rel.under_def by simp}
-     thus "rel.underS ?r' (a1,a2) \<le> (rel.under r ?m) \<times> (rel.under r ?m)" by auto
+     hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp}
+     thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto
   qed
-  moreover have "wo_rel.ofilter r (rel.under r ?m)"
+  moreover have "wo_rel.ofilter r (under r ?m)"
   using Well by (simp add: wo_rel.under_ofilter)
-  moreover have "rel.under r ?m < Field r"
-  using NE rel.under_Field[of r ?m] by blast
+  moreover have "under r ?m < Field r"
+  using NE under_Field[of r ?m] by blast
   ultimately show ?thesis by blast
 qed
 
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Order_Relation_More.thy
--- a/src/HOL/Cardinals/Order_Relation_More.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Order_Relation_More.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -14,66 +14,63 @@
 
 subsection {* The upper and lower bounds operators  *}
 
-context rel
-begin
-
-lemma aboveS_subset_above: "aboveS a \<le> above a"
+lemma aboveS_subset_above: "aboveS r a \<le> above r a"
 by(auto simp add: aboveS_def above_def)
 
-lemma AboveS_subset_Above: "AboveS A \<le> Above A"
+lemma AboveS_subset_Above: "AboveS r A \<le> Above r A"
 by(auto simp add: AboveS_def Above_def)
 
-lemma UnderS_disjoint: "A Int (UnderS A) = {}"
+lemma UnderS_disjoint: "A Int (UnderS r A) = {}"
 by(auto simp add: UnderS_def)
 
-lemma aboveS_notIn: "a \<notin> aboveS a"
+lemma aboveS_notIn: "a \<notin> aboveS r a"
 by(auto simp add: aboveS_def)
 
-lemma Refl_above_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> above a"
+lemma Refl_above_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> above r a"
 by(auto simp add: refl_on_def above_def)
 
-lemma in_Above_under: "a \<in> Field r \<Longrightarrow> a \<in> Above (under a)"
+lemma in_Above_under: "a \<in> Field r \<Longrightarrow> a \<in> Above r (under r a)"
 by(auto simp add: Above_def under_def)
 
-lemma in_Under_above: "a \<in> Field r \<Longrightarrow> a \<in> Under (above a)"
+lemma in_Under_above: "a \<in> Field r \<Longrightarrow> a \<in> Under r (above r a)"
 by(auto simp add: Under_def above_def)
 
-lemma in_UnderS_aboveS: "a \<in> Field r \<Longrightarrow> a \<in> UnderS (aboveS a)"
+lemma in_UnderS_aboveS: "a \<in> Field r \<Longrightarrow> a \<in> UnderS r (aboveS r a)"
 by(auto simp add: UnderS_def aboveS_def)
 
-lemma UnderS_subset_Under: "UnderS A \<le> Under A"
+lemma UnderS_subset_Under: "UnderS r A \<le> Under r A"
 by(auto simp add: UnderS_def Under_def)
 
-lemma subset_Above_Under: "B \<le> Field r \<Longrightarrow> B \<le> Above (Under B)"
+lemma subset_Above_Under: "B \<le> Field r \<Longrightarrow> B \<le> Above r (Under r B)"
 by(auto simp add: Above_def Under_def)
 
-lemma subset_Under_Above: "B \<le> Field r \<Longrightarrow> B \<le> Under (Above B)"
+lemma subset_Under_Above: "B \<le> Field r \<Longrightarrow> B \<le> Under r (Above r B)"
 by(auto simp add: Under_def Above_def)
 
-lemma subset_AboveS_UnderS: "B \<le> Field r \<Longrightarrow> B \<le> AboveS (UnderS B)"
+lemma subset_AboveS_UnderS: "B \<le> Field r \<Longrightarrow> B \<le> AboveS r (UnderS r B)"
 by(auto simp add: AboveS_def UnderS_def)
 
-lemma subset_UnderS_AboveS: "B \<le> Field r \<Longrightarrow> B \<le> UnderS (AboveS B)"
+lemma subset_UnderS_AboveS: "B \<le> Field r \<Longrightarrow> B \<le> UnderS r (AboveS r B)"
 by(auto simp add: UnderS_def AboveS_def)
 
 lemma Under_Above_Galois:
-"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> Above C) = (C \<le> Under B)"
+"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> Above r C) = (C \<le> Under r B)"
 by(unfold Above_def Under_def, blast)
 
 lemma UnderS_AboveS_Galois:
-"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> AboveS C) = (C \<le> UnderS B)"
+"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> AboveS r C) = (C \<le> UnderS r B)"
 by(unfold AboveS_def UnderS_def, blast)
 
 lemma Refl_above_aboveS:
-assumes REFL: "Refl r" and IN: "a \<in> Field r"
-shows "above a = aboveS a \<union> {a}"
+  assumes REFL: "Refl r" and IN: "a \<in> Field r"
+  shows "above r a = aboveS r a \<union> {a}"
 proof(unfold above_def aboveS_def, auto)
   show "(a,a) \<in> r" using REFL IN refl_on_def[of _ r] by blast
 qed
 
 lemma Linear_order_under_aboveS_Field:
-assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
-shows "Field r = under a \<union> aboveS a"
+  assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
+  shows "Field r = under r a \<union> aboveS r a"
 proof(unfold under_def aboveS_def, auto)
   assume "a \<in> Field r" "(a, a) \<notin> r"
   with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
@@ -96,7 +93,7 @@
 
 lemma Linear_order_underS_above_Field:
 assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
-shows "Field r = underS a \<union> above a"
+shows "Field r = underS r a \<union> above r a"
 proof(unfold underS_def above_def, auto)
   assume "a \<in> Field r" "(a, a) \<notin> r"
   with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
@@ -117,155 +114,155 @@
   using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
 qed
 
-lemma under_empty: "a \<notin> Field r \<Longrightarrow> under a = {}"
+lemma under_empty: "a \<notin> Field r \<Longrightarrow> under r a = {}"
 unfolding Field_def under_def by auto
 
-lemma Under_Field: "Under A \<le> Field r"
+lemma Under_Field: "Under r A \<le> Field r"
 by(unfold Under_def Field_def, auto)
 
-lemma UnderS_Field: "UnderS A \<le> Field r"
+lemma UnderS_Field: "UnderS r A \<le> Field r"
 by(unfold UnderS_def Field_def, auto)
 
-lemma above_Field: "above a \<le> Field r"
+lemma above_Field: "above r a \<le> Field r"
 by(unfold above_def Field_def, auto)
 
-lemma aboveS_Field: "aboveS a \<le> Field r"
+lemma aboveS_Field: "aboveS r a \<le> Field r"
 by(unfold aboveS_def Field_def, auto)
 
-lemma Above_Field: "Above A \<le> Field r"
+lemma Above_Field: "Above r A \<le> Field r"
 by(unfold Above_def Field_def, auto)
 
 lemma Refl_under_Under:
 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "Under A = (\<Inter> a \<in> A. under a)"
+shows "Under r A = (\<Inter> a \<in> A. under r a)"
 proof
-  show "Under A \<subseteq> (\<Inter> a \<in> A. under a)"
+  show "Under r A \<subseteq> (\<Inter> a \<in> A. under r a)"
   by(unfold Under_def under_def, auto)
 next
-  show "(\<Inter> a \<in> A. under a) \<subseteq> Under A"
+  show "(\<Inter> a \<in> A. under r a) \<subseteq> Under r A"
   proof(auto)
     fix x
-    assume *: "\<forall>xa \<in> A. x \<in> under xa"
+    assume *: "\<forall>xa \<in> A. x \<in> under r xa"
     hence "\<forall>xa \<in> A. (x,xa) \<in> r"
     by (simp add: under_def)
     moreover
     {from NE obtain a where "a \<in> A" by blast
-     with * have "x \<in> under a" by simp
+     with * have "x \<in> under r a" by simp
      hence "x \<in> Field r"
-     using under_Field[of a] by auto
+     using under_Field[of r a] by auto
     }
-    ultimately show "x \<in> Under A"
+    ultimately show "x \<in> Under r A"
     unfolding Under_def by auto
   qed
 qed
 
 lemma Refl_underS_UnderS:
 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "UnderS A = (\<Inter> a \<in> A. underS a)"
+shows "UnderS r A = (\<Inter> a \<in> A. underS r a)"
 proof
-  show "UnderS A \<subseteq> (\<Inter> a \<in> A. underS a)"
+  show "UnderS r A \<subseteq> (\<Inter> a \<in> A. underS r a)"
   by(unfold UnderS_def underS_def, auto)
 next
-  show "(\<Inter> a \<in> A. underS a) \<subseteq> UnderS A"
+  show "(\<Inter> a \<in> A. underS r a) \<subseteq> UnderS r A"
   proof(auto)
     fix x
-    assume *: "\<forall>xa \<in> A. x \<in> underS xa"
+    assume *: "\<forall>xa \<in> A. x \<in> underS r xa"
     hence "\<forall>xa \<in> A. x \<noteq> xa \<and> (x,xa) \<in> r"
     by (auto simp add: underS_def)
     moreover
     {from NE obtain a where "a \<in> A" by blast
-     with * have "x \<in> underS a" by simp
+     with * have "x \<in> underS r a" by simp
      hence "x \<in> Field r"
-     using underS_Field[of a] by auto
+     using underS_Field[of r a] by auto
     }
-    ultimately show "x \<in> UnderS A"
+    ultimately show "x \<in> UnderS r A"
     unfolding UnderS_def by auto
   qed
 qed
 
 lemma Refl_above_Above:
 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "Above A = (\<Inter> a \<in> A. above a)"
+shows "Above r A = (\<Inter> a \<in> A. above r a)"
 proof
-  show "Above A \<subseteq> (\<Inter> a \<in> A. above a)"
+  show "Above r A \<subseteq> (\<Inter> a \<in> A. above r a)"
   by(unfold Above_def above_def, auto)
 next
-  show "(\<Inter> a \<in> A. above a) \<subseteq> Above A"
+  show "(\<Inter> a \<in> A. above r a) \<subseteq> Above r A"
   proof(auto)
     fix x
-    assume *: "\<forall>xa \<in> A. x \<in> above xa"
+    assume *: "\<forall>xa \<in> A. x \<in> above r xa"
     hence "\<forall>xa \<in> A. (xa,x) \<in> r"
     by (simp add: above_def)
     moreover
     {from NE obtain a where "a \<in> A" by blast
-     with * have "x \<in> above a" by simp
+     with * have "x \<in> above r a" by simp
      hence "x \<in> Field r"
-     using above_Field[of a] by auto
+     using above_Field[of r a] by auto
     }
-    ultimately show "x \<in> Above A"
+    ultimately show "x \<in> Above r A"
     unfolding Above_def by auto
   qed
 qed
 
 lemma Refl_aboveS_AboveS:
 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "AboveS A = (\<Inter> a \<in> A. aboveS a)"
+shows "AboveS r A = (\<Inter> a \<in> A. aboveS r a)"
 proof
-  show "AboveS A \<subseteq> (\<Inter> a \<in> A. aboveS a)"
+  show "AboveS r A \<subseteq> (\<Inter> a \<in> A. aboveS r a)"
   by(unfold AboveS_def aboveS_def, auto)
 next
-  show "(\<Inter> a \<in> A. aboveS a) \<subseteq> AboveS A"
+  show "(\<Inter> a \<in> A. aboveS r a) \<subseteq> AboveS r A"
   proof(auto)
     fix x
-    assume *: "\<forall>xa \<in> A. x \<in> aboveS xa"
+    assume *: "\<forall>xa \<in> A. x \<in> aboveS r xa"
     hence "\<forall>xa \<in> A. xa \<noteq> x \<and> (xa,x) \<in> r"
     by (auto simp add: aboveS_def)
     moreover
     {from NE obtain a where "a \<in> A" by blast
-     with * have "x \<in> aboveS a" by simp
+     with * have "x \<in> aboveS r a" by simp
      hence "x \<in> Field r"
-     using aboveS_Field[of a] by auto
+     using aboveS_Field[of r a] by auto
     }
-    ultimately show "x \<in> AboveS A"
+    ultimately show "x \<in> AboveS r A"
     unfolding AboveS_def by auto
   qed
 qed
 
-lemma under_Under_singl: "under a = Under {a}"
+lemma under_Under_singl: "under r a = Under r {a}"
 by(unfold Under_def under_def, auto simp add: Field_def)
 
-lemma underS_UnderS_singl: "underS a = UnderS {a}"
+lemma underS_UnderS_singl: "underS r a = UnderS r {a}"
 by(unfold UnderS_def underS_def, auto simp add: Field_def)
 
-lemma above_Above_singl: "above a = Above {a}"
+lemma above_Above_singl: "above r a = Above r {a}"
 by(unfold Above_def above_def, auto simp add: Field_def)
 
-lemma aboveS_AboveS_singl: "aboveS a = AboveS {a}"
+lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}"
 by(unfold AboveS_def aboveS_def, auto simp add: Field_def)
 
-lemma Under_decr: "A \<le> B \<Longrightarrow> Under B \<le> Under A"
+lemma Under_decr: "A \<le> B \<Longrightarrow> Under r B \<le> Under r A"
 by(unfold Under_def, auto)
 
-lemma UnderS_decr: "A \<le> B \<Longrightarrow> UnderS B \<le> UnderS A"
+lemma UnderS_decr: "A \<le> B \<Longrightarrow> UnderS r B \<le> UnderS r A"
 by(unfold UnderS_def, auto)
 
-lemma Above_decr: "A \<le> B \<Longrightarrow> Above B \<le> Above A"
+lemma Above_decr: "A \<le> B \<Longrightarrow> Above r B \<le> Above r A"
 by(unfold Above_def, auto)
 
-lemma AboveS_decr: "A \<le> B \<Longrightarrow> AboveS B \<le> AboveS A"
+lemma AboveS_decr: "A \<le> B \<Longrightarrow> AboveS r B \<le> AboveS r A"
 by(unfold AboveS_def, auto)
 
 lemma under_incl_iff:
 assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \<in> Field r"
-shows "(under a \<le> under b) = ((a,b) \<in> r)"
+shows "(under r a \<le> under r b) = ((a,b) \<in> r)"
 proof
   assume "(a,b) \<in> r"
-  thus "under a \<le> under b" using TRANS
+  thus "under r a \<le> under r b" using TRANS
   by (auto simp add: under_incr)
 next
-  assume "under a \<le> under b"
+  assume "under r a \<le> under r b"
   moreover
-  have "a \<in> under a" using REFL IN
+  have "a \<in> under r a" using REFL IN
   by (auto simp add: Refl_under_in)
   ultimately show "(a,b) \<in> r"
   by (auto simp add: under_def)
@@ -273,7 +270,7 @@
 
 lemma above_decr:
 assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
-shows "above b \<le> above a"
+shows "above r b \<le> above r a"
 proof(unfold above_def, auto)
   fix x assume "(b,x) \<in> r"
   with REL TRANS trans_def[of r]
@@ -283,7 +280,7 @@
 lemma aboveS_decr:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
         REL: "(a,b) \<in> r"
-shows "aboveS b \<le> aboveS a"
+shows "aboveS r b \<le> aboveS r a"
 proof(unfold aboveS_def, auto)
   assume *: "a \<noteq> b" and **: "(b,a) \<in> r"
   with ANTISYM antisym_def[of r] REL
@@ -296,11 +293,11 @@
 
 lemma under_trans:
 assumes TRANS: "trans r" and
-        IN1: "a \<in> under b" and IN2: "b \<in> under c"
-shows "a \<in> under c"
+        IN1: "a \<in> under r b" and IN2: "b \<in> under r c"
+shows "a \<in> under r c"
 proof-
   have "(a,b) \<in> r \<and> (b,c) \<in> r"
-  using IN1 IN2 under_def by auto
+  using IN1 IN2 under_def by fastforce
   hence "(a,c) \<in> r"
   using TRANS trans_def[of r] by blast
   thus ?thesis unfolding under_def by simp
@@ -308,14 +305,14 @@
 
 lemma under_underS_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "a \<in> under b" and IN2: "b \<in> underS c"
-shows "a \<in> underS c"
+        IN1: "a \<in> under r b" and IN2: "b \<in> underS r c"
+shows "a \<in> underS r c"
 proof-
   have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
-  using IN1 IN2 under_def underS_def by auto
+  using IN1 IN2 under_def underS_def by fastforce
   hence 1: "(a,c) \<in> r"
   using TRANS trans_def[of r] by blast
-  have 2: "b \<noteq> c" using IN2 underS_def by auto
+  have 2: "b \<noteq> c" using IN2 underS_def by force
   have 3: "a \<noteq> c"
   proof
     assume "a = c" with 0 2 ANTISYM antisym_def[of r]
@@ -326,14 +323,14 @@
 
 lemma underS_under_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "a \<in> underS b" and IN2: "b \<in> under c"
-shows "a \<in> underS c"
+        IN1: "a \<in> underS r b" and IN2: "b \<in> under r c"
+shows "a \<in> underS r c"
 proof-
   have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
-  using IN1 IN2 under_def underS_def by auto
+  using IN1 IN2 under_def underS_def by fast
   hence 1: "(a,c) \<in> r"
-  using TRANS trans_def[of r] by blast
-  have 2: "a \<noteq> b" using IN1 underS_def by auto
+  using TRANS trans_def[of r] by fast
+  have 2: "a \<noteq> b" using IN1 underS_def by force
   have 3: "a \<noteq> c"
   proof
     assume "a = c" with 0 2 ANTISYM antisym_def[of r]
@@ -344,21 +341,21 @@
 
 lemma underS_underS_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "a \<in> underS b" and IN2: "b \<in> underS c"
-shows "a \<in> underS c"
+        IN1: "a \<in> underS r b" and IN2: "b \<in> underS r c"
+shows "a \<in> underS r c"
 proof-
-  have "a \<in> under b"
-  using IN1 underS_subset_under by auto
-  with assms under_underS_trans show ?thesis by auto
+  have "a \<in> under r b"
+  using IN1 underS_subset_under by fast
+  with assms under_underS_trans show ?thesis by fast
 qed
 
 lemma above_trans:
 assumes TRANS: "trans r" and
-        IN1: "b \<in> above a" and IN2: "c \<in> above b"
-shows "c \<in> above a"
+        IN1: "b \<in> above r a" and IN2: "c \<in> above r b"
+shows "c \<in> above r a"
 proof-
   have "(a,b) \<in> r \<and> (b,c) \<in> r"
-  using IN1 IN2 above_def by auto
+  using IN1 IN2 above_def by fast
   hence "(a,c) \<in> r"
   using TRANS trans_def[of r] by blast
   thus ?thesis unfolding above_def by simp
@@ -366,14 +363,14 @@
 
 lemma above_aboveS_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "b \<in> above a" and IN2: "c \<in> aboveS b"
-shows "c \<in> aboveS a"
+        IN1: "b \<in> above r a" and IN2: "c \<in> aboveS r b"
+shows "c \<in> aboveS r a"
 proof-
   have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
-  using IN1 IN2 above_def aboveS_def by auto
+  using IN1 IN2 above_def aboveS_def by fast
   hence 1: "(a,c) \<in> r"
   using TRANS trans_def[of r] by blast
-  have 2: "b \<noteq> c" using IN2 aboveS_def by auto
+  have 2: "b \<noteq> c" using IN2 aboveS_def by force
   have 3: "a \<noteq> c"
   proof
     assume "a = c" with 0 2 ANTISYM antisym_def[of r]
@@ -384,14 +381,14 @@
 
 lemma aboveS_above_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "b \<in> aboveS a" and IN2: "c \<in> above b"
-shows "c \<in> aboveS a"
+        IN1: "b \<in> aboveS r a" and IN2: "c \<in> above r b"
+shows "c \<in> aboveS r a"
 proof-
   have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
-  using IN1 IN2 above_def aboveS_def by auto
+  using IN1 IN2 above_def aboveS_def by fast
   hence 1: "(a,c) \<in> r"
   using TRANS trans_def[of r] by blast
-  have 2: "a \<noteq> b" using IN1 aboveS_def by auto
+  have 2: "a \<noteq> b" using IN1 aboveS_def by force
   have 3: "a \<noteq> c"
   proof
     assume "a = c" with 0 2 ANTISYM antisym_def[of r]
@@ -402,21 +399,23 @@
 
 lemma aboveS_aboveS_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "b \<in> aboveS a" and IN2: "c \<in> aboveS b"
-shows "c \<in> aboveS a"
+        IN1: "b \<in> aboveS r a" and IN2: "c \<in> aboveS r b"
+shows "c \<in> aboveS r a"
 proof-
-  have "b \<in> above a"
-  using IN1 aboveS_subset_above by auto
-  with assms above_aboveS_trans show ?thesis by auto
+  have "b \<in> above r a"
+  using IN1 aboveS_subset_above by fast
+  with assms above_aboveS_trans show ?thesis by fast
 qed
 
 lemma under_Under_trans:
 assumes TRANS: "trans r" and
-        IN1: "a \<in> under b" and IN2: "b \<in> Under C"
-shows "a \<in> Under C"
+        IN1: "a \<in> under r b" and IN2: "b \<in> Under r C"
+shows "a \<in> Under r C"
 proof-
-  have "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
-  using IN1 IN2 under_def Under_def by blast
+  have "b \<in> {u \<in> Field r. \<forall>x. x \<in> C \<longrightarrow> (u, x) \<in> r}"
+    using IN2 Under_def by force
+  hence "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
+    using IN1 under_def by fast
   hence "\<forall>c \<in> C. (a,c) \<in> r"
   using TRANS trans_def[of r] by blast
   moreover
@@ -427,22 +426,22 @@
 
 lemma underS_Under_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "a \<in> underS b" and IN2: "b \<in> Under C"
-shows "a \<in> UnderS C"
+        IN1: "a \<in> underS r b" and IN2: "b \<in> Under r C"
+shows "a \<in> UnderS r C"
 proof-
-  from IN1 have "a \<in> under b"
-  using underS_subset_under[of b] by blast
+  from IN1 have "a \<in> under r b"
+  using underS_subset_under[of r b] by fast
   with assms under_Under_trans
-  have "a \<in> Under C" by auto
+  have "a \<in> Under r C" by fast
   (*  *)
   moreover
   have "a \<notin> C"
   proof
     assume *: "a \<in> C"
     have 1: "b \<noteq> a \<and> (a,b) \<in> r"
-    using IN1 underS_def[of b] by auto
+    using IN1 underS_def[of r b] by auto
     have "\<forall>c \<in> C. (b,c) \<in> r"
-    using IN2 Under_def[of C] by auto
+    using IN2 Under_def[of r C] by auto
     with * have "(b,a) \<in> r" by simp
     with 1 ANTISYM antisym_def[of r]
     show False by blast
@@ -450,53 +449,53 @@
   (*  *)
   ultimately
   show ?thesis unfolding UnderS_def
-  using Under_def by auto
+  using Under_def by force
 qed
 
 lemma underS_UnderS_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "a \<in> underS b" and IN2: "b \<in> UnderS C"
-shows "a \<in> UnderS C"
+        IN1: "a \<in> underS r b" and IN2: "b \<in> UnderS r C"
+shows "a \<in> UnderS r C"
 proof-
-  from IN2 have "b \<in> Under C"
-  using UnderS_subset_Under[of C] by blast
+  from IN2 have "b \<in> Under r C"
+  using UnderS_subset_Under[of r C] by blast
   with underS_Under_trans assms
-  show ?thesis by auto
+  show ?thesis by force
 qed
 
 lemma above_Above_trans:
 assumes TRANS: "trans r" and
-        IN1: "a \<in> above b" and IN2: "b \<in> Above C"
-shows "a \<in> Above C"
+        IN1: "a \<in> above r b" and IN2: "b \<in> Above r C"
+shows "a \<in> Above r C"
 proof-
   have "(b,a) \<in> r \<and> (\<forall>c \<in> C. (c,b) \<in> r)"
-  using IN1 IN2 above_def Above_def by auto
+    using IN1[unfolded above_def] IN2[unfolded Above_def] by simp
   hence "\<forall>c \<in> C. (c,a) \<in> r"
   using TRANS trans_def[of r] by blast
   moreover
-  have "a \<in> Field r" using IN1 Field_def above_def by force
+  have "a \<in> Field r" using IN1[unfolded above_def] Field_def by fast
   ultimately
   show ?thesis unfolding Above_def by auto
 qed
 
 lemma aboveS_Above_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "a \<in> aboveS b" and IN2: "b \<in> Above C"
-shows "a \<in> AboveS C"
+        IN1: "a \<in> aboveS r b" and IN2: "b \<in> Above r C"
+shows "a \<in> AboveS r C"
 proof-
-  from IN1 have "a \<in> above b"
-  using aboveS_subset_above[of b] by blast
+  from IN1 have "a \<in> above r b"
+  using aboveS_subset_above[of r b] by blast
   with assms above_Above_trans
-  have "a \<in> Above C" by auto
+  have "a \<in> Above r C" by fast
   (*  *)
   moreover
   have "a \<notin> C"
   proof
     assume *: "a \<in> C"
     have 1: "b \<noteq> a \<and> (b,a) \<in> r"
-    using IN1 aboveS_def[of b] by auto
+    using IN1 aboveS_def[of r b] by auto
     have "\<forall>c \<in> C. (c,b) \<in> r"
-    using IN2 Above_def[of C] by auto
+    using IN2 Above_def[of r C] by auto
     with * have "(a,b) \<in> r" by simp
     with 1 ANTISYM antisym_def[of r]
     show False by blast
@@ -504,27 +503,27 @@
   (*  *)
   ultimately
   show ?thesis unfolding AboveS_def
-  using Above_def by auto
+  using Above_def by force
 qed
 
 lemma above_AboveS_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "a \<in> above b" and IN2: "b \<in> AboveS C"
-shows "a \<in> AboveS C"
+        IN1: "a \<in> above r b" and IN2: "b \<in> AboveS r C"
+shows "a \<in> AboveS r C"
 proof-
-  from IN2 have "b \<in> Above C"
-  using AboveS_subset_Above[of C] by blast
+  from IN2 have "b \<in> Above r C"
+  using AboveS_subset_Above[of r C] by blast
   with assms above_Above_trans
-  have "a \<in> Above C" by auto
+  have "a \<in> Above r C" by force
   (*  *)
   moreover
   have "a \<notin> C"
   proof
     assume *: "a \<in> C"
     have 1: "(b,a) \<in> r"
-    using IN1 above_def[of b] by auto
+    using IN1 above_def[of r b] by auto
     have "\<forall>c \<in> C. b \<noteq> c \<and> (c,b) \<in> r"
-    using IN2 AboveS_def[of C] by auto
+    using IN2 AboveS_def[of r C] by auto
     with * have "b \<noteq> a \<and> (a,b) \<in> r" by simp
     with 1 ANTISYM antisym_def[of r]
     show False by blast
@@ -532,38 +531,38 @@
   (*  *)
   ultimately
   show ?thesis unfolding AboveS_def
-  using Above_def by auto
+  using Above_def by force
 qed
 
 lemma aboveS_AboveS_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "a \<in> aboveS b" and IN2: "b \<in> AboveS C"
-shows "a \<in> AboveS C"
+        IN1: "a \<in> aboveS r b" and IN2: "b \<in> AboveS r C"
+shows "a \<in> AboveS r C"
 proof-
-  from IN2 have "b \<in> Above C"
-  using AboveS_subset_Above[of C] by blast
+  from IN2 have "b \<in> Above r C"
+  using AboveS_subset_Above[of r C] by blast
   with aboveS_Above_trans assms
-  show ?thesis by auto
+  show ?thesis by force
 qed
 
 lemma under_UnderS_trans:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
-        IN1: "a \<in> under b" and IN2: "b \<in> UnderS C"
-shows "a \<in> UnderS C"
+        IN1: "a \<in> under r b" and IN2: "b \<in> UnderS r C"
+shows "a \<in> UnderS r C"
 proof-
-  from IN2 have "b \<in> Under C"
-  using UnderS_subset_Under[of C] by blast
+  from IN2 have "b \<in> Under r C"
+  using UnderS_subset_Under[of r C] by blast
   with assms under_Under_trans
-  have "a \<in> Under C" by blast
+  have "a \<in> Under r C" by force
   (*  *)
   moreover
   have "a \<notin> C"
   proof
     assume *: "a \<in> C"
     have 1: "(a,b) \<in> r"
-    using IN1 under_def[of b] by auto
+    using IN1 under_def[of r b] by auto
     have "\<forall>c \<in> C. b \<noteq> c \<and> (b,c) \<in> r"
-    using IN2 UnderS_def[of C] by blast
+    using IN2 UnderS_def[of r C] by blast
     with * have "b \<noteq> a \<and> (b,a) \<in> r" by blast
     with 1 ANTISYM antisym_def[of r]
     show False by blast
@@ -573,66 +572,59 @@
   show ?thesis unfolding UnderS_def Under_def by fast
 qed
 
-end  (* context rel *)
-
 
 subsection {* Properties depending on more than one relation  *}
 
-abbreviation "under \<equiv> rel.under"
-abbreviation "underS \<equiv> rel.underS"
-abbreviation "Under \<equiv> rel.Under"
-abbreviation "UnderS \<equiv> rel.UnderS"
-abbreviation "above \<equiv> rel.above"
-abbreviation "aboveS \<equiv> rel.aboveS"
-abbreviation "Above \<equiv> rel.Above"
-abbreviation "AboveS \<equiv> rel.AboveS"
-
 lemma under_incr2:
 "r \<le> r' \<Longrightarrow> under r a \<le> under r' a"
-unfolding rel.under_def by blast
+unfolding under_def by blast
 
 lemma underS_incr2:
 "r \<le> r' \<Longrightarrow> underS r a \<le> underS r' a"
-unfolding rel.underS_def by blast
+unfolding underS_def by blast
 
+(* FIXME: r \<leadsto> r'
 lemma Under_incr:
 "r \<le> r' \<Longrightarrow> Under r A \<le> Under r A"
-unfolding rel.Under_def by blast
+unfolding Under_def by blast
 
 lemma UnderS_incr:
 "r \<le> r' \<Longrightarrow> UnderS r A \<le> UnderS r A"
-unfolding rel.UnderS_def by blast
+unfolding UnderS_def by blast
 
 lemma Under_incr_decr:
 "\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> Under r A \<le> Under r A'"
-unfolding rel.Under_def by blast
+unfolding Under_def by blast
 
 lemma UnderS_incr_decr:
 "\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> UnderS r A \<le> UnderS r A'"
-unfolding rel.UnderS_def by blast
+unfolding UnderS_def by blast
+*)
 
 lemma above_incr2:
 "r \<le> r' \<Longrightarrow> above r a \<le> above r' a"
-unfolding rel.above_def by blast
+unfolding above_def by blast
 
 lemma aboveS_incr2:
 "r \<le> r' \<Longrightarrow> aboveS r a \<le> aboveS r' a"
-unfolding rel.aboveS_def by blast
+unfolding aboveS_def by blast
 
+(* FIXME
 lemma Above_incr:
 "r \<le> r' \<Longrightarrow> Above r A \<le> Above r A"
-unfolding rel.Above_def by blast
+unfolding Above_def by blast
 
 lemma AboveS_incr:
 "r \<le> r' \<Longrightarrow> AboveS r A \<le> AboveS r A"
-unfolding rel.AboveS_def by blast
+unfolding AboveS_def by blast
 
 lemma Above_incr_decr:
-"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> Above r A \<le> Above r A'"
-unfolding rel.Above_def by blast
+"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> Above r A \<le> Above r A'"
+unfolding Above_def by blast
 
 lemma AboveS_incr_decr:
-"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> AboveS r A \<le> AboveS r A'"
-unfolding rel.AboveS_def by blast
+"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> AboveS r A \<le> AboveS r A'"
+unfolding AboveS_def by blast
+*)
 
 end
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Order_Relation_More_FP.thy
--- a/src/HOL/Cardinals/Order_Relation_More_FP.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Order_Relation_More_FP.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -19,16 +19,6 @@
 further define upper and lower bounds operators. *}
 
 
-locale rel = fixes r :: "'a rel"
-
-text{* The following context encompasses all this section, except
-for its last subsection. In other words, for the rest of this section except its last
-subsection, we consider a fixed relation @{text "r"}. *}
-
-context rel
-begin
-
-
 subsection {* Auxiliaries *}
 
 
@@ -39,7 +29,7 @@
 
 corollary well_order_on_domain:
 "\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
-by(simp add: refl_on_domain order_on_defs)
+by (auto simp add: refl_on_domain order_on_defs)
 
 
 lemma well_order_on_Field:
@@ -49,7 +39,7 @@
 
 lemma well_order_on_Well_order:
 "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
-using well_order_on_Field by simp
+using well_order_on_Field by auto
 
 
 lemma Total_subset_Id:
@@ -91,103 +81,91 @@
 Capitalization of the first letter in the name reminds that the operator acts on sets, rather
 than on individual elements. *}
 
-definition under::"'a \<Rightarrow> 'a set"
-where "under a \<equiv> {b. (b,a) \<in> r}"
+definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+where "under r a \<equiv> {b. (b,a) \<in> r}"
 
-definition underS::"'a \<Rightarrow> 'a set"
-where "underS a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
+definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+where "underS r a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
 
-definition Under::"'a set \<Rightarrow> 'a set"
-where "Under A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
+definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
 
-definition UnderS::"'a set \<Rightarrow> 'a set"
-where "UnderS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
+definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
 
-definition above::"'a \<Rightarrow> 'a set"
-where "above a \<equiv> {b. (a,b) \<in> r}"
+definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+where "above r a \<equiv> {b. (a,b) \<in> r}"
 
-definition aboveS::"'a \<Rightarrow> 'a set"
-where "aboveS a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
+definition aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
 
-definition Above::"'a set \<Rightarrow> 'a set"
-where "Above A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
+definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
 
-definition AboveS::"'a set \<Rightarrow> 'a set"
-where "AboveS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
-(*  *)
+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}"
 
 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. *}
 
-
-lemma underS_subset_under: "underS a \<le> under a"
+lemma underS_subset_under: "underS r a \<le> under r a"
 by(auto simp add: underS_def under_def)
 
 
-lemma underS_notIn: "a \<notin> underS a"
+lemma underS_notIn: "a \<notin> underS r a"
 by(simp add: underS_def)
 
 
-lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under a"
+lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a"
 by(simp add: refl_on_def under_def)
 
 
-lemma AboveS_disjoint: "A Int (AboveS A) = {}"
+lemma AboveS_disjoint: "A Int (AboveS r A) = {}"
 by(auto simp add: AboveS_def)
 
-
-lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS (underS a)"
+lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
 by(auto simp add: AboveS_def underS_def)
 
-
 lemma Refl_under_underS:
-assumes "Refl r" "a \<in> Field r"
-shows "under a = underS a \<union> {a}"
+  assumes "Refl r" "a \<in> Field r"
+  shows "under r a = underS r a \<union> {a}"
 unfolding under_def underS_def
 using assms refl_on_def[of _ r] by fastforce
 
-
-lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS a = {}"
+lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
 by (auto simp: Field_def underS_def)
 
-
-lemma under_Field: "under a \<le> Field r"
+lemma under_Field: "under r a \<le> Field r"
 by(unfold under_def Field_def, auto)
 
-
-lemma underS_Field: "underS a \<le> Field r"
+lemma underS_Field: "underS r a \<le> Field r"
 by(unfold underS_def Field_def, auto)
 
-
 lemma underS_Field2:
-"a \<in> Field r \<Longrightarrow> underS a < Field r"
-using assms underS_notIn underS_Field by blast
-
+"a \<in> Field r \<Longrightarrow> underS r a < Field r"
+using underS_notIn underS_Field by fast
 
 lemma underS_Field3:
-"Field r \<noteq> {} \<Longrightarrow> underS a < Field r"
+"Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"
 by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
 
-
-lemma AboveS_Field: "AboveS A \<le> Field r"
+lemma AboveS_Field: "AboveS r A \<le> Field r"
 by(unfold AboveS_def Field_def, auto)
 
-
 lemma under_incr:
-assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
-shows "under a \<le> under b"
+  assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
+  shows "under r a \<le> under r b"
 proof(unfold under_def, auto)
   fix x assume "(x,a) \<in> r"
   with REL TRANS trans_def[of r]
   show "(x,b) \<in> r" by blast
 qed
 
-
 lemma underS_incr:
 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
         REL: "(a,b) \<in> r"
-shows "underS a \<le> underS b"
+shows "underS r a \<le> underS r b"
 proof(unfold underS_def, auto)
   assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
   with ANTISYM antisym_def[of r] REL
@@ -198,25 +176,24 @@
   show "(x,b) \<in> r" by blast
 qed
 
-
 lemma underS_incl_iff:
 assumes LO: "Linear_order r" and
         INa: "a \<in> Field r" and INb: "b \<in> Field r"
-shows "(underS a \<le> underS b) = ((a,b) \<in> r)"
+shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)"
 proof
   assume "(a,b) \<in> r"
-  thus "underS a \<le> underS b" using LO
+  thus "underS r a \<le> underS r b" using LO
   by (simp add: order_on_defs underS_incr)
 next
-  assume *: "underS a \<le> underS b"
+  assume *: "underS r a \<le> underS r b"
   {assume "a = b"
    hence "(a,b) \<in> r" using assms
    by (simp add: order_on_defs refl_on_def)
   }
   moreover
   {assume "a \<noteq> b \<and> (b,a) \<in> r"
-   hence "b \<in> underS a" unfolding underS_def by blast
-   hence "b \<in> underS b" using * by blast
+   hence "b \<in> underS r a" unfolding underS_def by blast
+   hence "b \<in> underS r b" using * by blast
    hence False by (simp add: underS_notIn)
   }
   ultimately
@@ -224,7 +201,4 @@
   order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
 qed
 
-
-end  (* context rel *)
-
 end
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -148,7 +148,7 @@
   have "compat r (r +o r') Inl" unfolding compat_def osum_def by auto
   moreover
   have "ofilter (r +o r') (Inl ` Field r)"
-    unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum rel.under_def
+    unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum under_def
     unfolding osum_def Field_def by auto
   ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
 qed
@@ -322,7 +322,7 @@
   from r' have "compat r (r *o r') ?f"  unfolding compat_def oprod_def by auto
   moreover
   from * have "ofilter (r *o r') (?f ` Field r)"
-    unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod rel.under_def
+    unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod under_def
     unfolding oprod_def by auto (auto simp: image_iff Field_def)
   moreover have "inj_on ?f (Field r)" unfolding inj_on_def by auto
   ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
@@ -924,11 +924,11 @@
 
 lemma iso_ozero_empty[simp]: "r =o ozero = (r = {})"
   unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def 
-  by (auto dest: rel.well_order_on_domain)
+  by (auto dest: well_order_on_domain)
 
 lemma ozero_ordLeq: 
 assumes "Well_order r"  shows "ozero \<le>o r"
-using assms unfolding ozero_def ordLeq_def embed_def[abs_def] rel.under_def by auto
+using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto
 
 definition "oone = {((),())}"
 
@@ -942,10 +942,10 @@
 lemma oone_ordIso: "oone =o {(x,x)}"
   unfolding ordIso_def oone_def well_order_on_def linear_order_on_def partial_order_on_def
     preorder_on_def total_on_def refl_on_def trans_def antisym_def
-  by (auto simp: iso_def embed_def bij_betw_def rel.under_def inj_on_def intro!: exI[of _ "\<lambda>_. x"])
+  by (auto simp: iso_def embed_def bij_betw_def under_def inj_on_def intro!: exI[of _ "\<lambda>_. x"])
 
 lemma osum_ordLeqR: "Well_order r \<Longrightarrow> Well_order s \<Longrightarrow> s \<le>o r +o s"
-  unfolding ordLeq_def2 rel.underS_def
+  unfolding ordLeq_def2 underS_def
   by (auto intro!: exI[of _ Inr] osum_Well_order) (auto simp add: osum_def Field_def)
 
 lemma osum_congL:
@@ -1043,7 +1043,7 @@
     unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
   with f have "bij_betw ?f (Field ?L) (Field ?R)"
     unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on)
-  moreover from f rel.well_order_on_domain[OF r] have "compat ?L ?R ?f"
+  moreover from f well_order_on_domain[OF r] have "compat ?L ?R ?f"
     unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
     by (auto simp: map_pair_imageI dest: inj_onD)
   ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
@@ -1057,7 +1057,7 @@
   assms[unfolded ordIso_def] by auto
 
 lemma Field_singleton[simp]: "Field {(z,z)} = {z}"
-  by (metis rel.well_order_on_Field well_order_on_singleton)
+  by (metis well_order_on_Field well_order_on_singleton)
 
 lemma zero_singleton[simp]: "zero {(z,z)} = z"
   using wo_rel.zero_in_Field[unfolded wo_rel_def, of "{(z, z)}"] well_order_on_singleton[of z]
@@ -1077,7 +1077,7 @@
   then obtain x where "x \<in> Field r" by auto
   with * have Fr: "Field r = {x}" by auto
   interpret r: wo_rel r by unfold_locales (rule r)
-  from Fr r.well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast
+  from Fr well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast
   interpret wo_rel2 r s by unfold_locales (rule r, rule s)
   have "bij_betw (\<lambda>x. ()) (Field ?L) (Field ?R)"
     unfolding bij_betw_def Field_oexp by (auto simp: r_def FinFunc_singleton)
@@ -1138,7 +1138,7 @@
   interpret t!: wo_rel t by unfold_locales (rule t)
   interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
   from *(3) have "ofilter ?R (?f ` Field ?L)"
-    unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image rel.under_def
+    unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image under_def
     by (auto simp: osum_def intro!: imageI) (auto simp: Field_def)
   ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
     by (auto intro: osum_Well_order r s t)
@@ -1157,7 +1157,7 @@
   let ?f = "sum_map f id"
   from f have "\<forall>a\<in>Field (r +o t).
      ?f a \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> underS (s +o t) (?f a)"
-     unfolding Field_osum rel.underS_def by (fastforce simp: osum_def)
+     unfolding Field_osum underS_def by (fastforce simp: osum_def)
   thus ?thesis unfolding ordLeq_def2 by (auto intro: osum_Well_order r s t)
 qed
 
@@ -1199,13 +1199,13 @@
   from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce
   moreover
   from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def
-    by auto (metis rel.well_order_on_domain t, metis rel.well_order_on_domain s)
+    by auto (metis well_order_on_domain t, metis well_order_on_domain s)
   moreover
   interpret t!: wo_rel t by unfold_locales (rule t)
   interpret rt!: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
   from *(3) have "ofilter ?R (?f ` Field ?L)"
-    unfolding t.ofilter_def rt.ofilter_def Field_oprod rel.under_def
-    by (auto simp: oprod_def image_iff) (fast | metis r rel.well_order_on_domain)+
+    unfolding t.ofilter_def rt.ofilter_def Field_oprod under_def
+    by (auto simp: oprod_def image_iff) (fast | metis r well_order_on_domain)+
   ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
     by (auto intro: oprod_Well_order r s t)
   moreover
@@ -1226,7 +1226,7 @@
   let ?f = "map_pair f id"
   from f have "\<forall>a\<in>Field (r *o t).
      ?f a \<in> Field (s *o t) \<and> ?f ` underS (r *o t) a \<subseteq> underS (s *o t) (?f a)"
-     unfolding Field_oprod rel.underS_def unfolding map_pair_def oprod_def by auto
+     unfolding Field_oprod underS_def unfolding map_pair_def oprod_def by auto
   thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t)
 qed
 
@@ -1269,7 +1269,7 @@
 
 lemma ozero_oexp: "\<not> (s =o ozero) \<Longrightarrow> ozero ^o s =o ozero"
   unfolding oexp_def[OF ozero_Well_order s] FinFunc_def
-  by simp (metis Func_emp2 bot.extremum_uniqueI emptyE rel.well_order_on_domain s subrelI)
+  by simp (metis Func_emp2 bot.extremum_uniqueI emptyE well_order_on_domain s subrelI)
       
 lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R")
   by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s])
@@ -1326,7 +1326,7 @@
   qed
   moreover
   from FLR have "ofilter ?R (F ` Field ?L)"
-  unfolding rexpt.ofilter_def rel.under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
+  unfolding rexpt.ofilter_def under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
   proof (safe elim!: imageI)
     fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r t" "F g \<in> FinFunc r t"
       "let m = t.max_fun_diff h (F g) in (h m, F g m) \<in> r"
@@ -1348,7 +1348,7 @@
           assume "(t.max_fun_diff h (F g), z) \<notin> t"
           hence "(z, t.max_fun_diff h (F g)) \<in> t" using t.in_notinI[of "t.max_fun_diff h (F g)" z]
             z max_Field by auto
-          hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def rel.under_def
+          hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def under_def
             by fastforce
           with z show False by blast
         qed
@@ -1356,9 +1356,9 @@
           z max_f_Field unfolding F_def by auto
       } note ** = this
       with *(3) gh(2) have "h = F (\<lambda>x. if x \<in> Field s then h (f x) else undefined)" using invff
-        unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def rel.under_def by auto
+        unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def under_def by auto
       moreover from gh(2) *(1,3) have "(\<lambda>x. if x \<in> Field s then h (f x) else undefined) \<in> FinFunc r s"
-        unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def rel.under_def
+        unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def under_def
         by (auto intro: subset_inj_on elim!: finite_imageD[OF finite_subset[rotated]])
       ultimately show "?thesis" by (rule image_eqI)
     qed simp
@@ -1396,7 +1396,7 @@
   interpret t!: wo_rel t by unfold_locales (rule t)
   show ?thesis
   proof (cases "t = {}")
-    case True thus ?thesis using r s unfolding ordLeq_def2 rel.underS_def by auto
+    case True thus ?thesis using r s unfolding ordLeq_def2 underS_def by auto
   next
     case False thus ?thesis
     proof (cases "r = {}")
@@ -1408,9 +1408,9 @@
       hence f_underS: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
         using embed_in_Field[OF rt.rWELL f] embed_underS2[OF rt.rWELL st.rWELL f] by auto
       from f `t \<noteq> {}` False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}"
-        unfolding Field_def embed_def rel.under_def bij_betw_def by auto
+        unfolding Field_def embed_def under_def bij_betw_def by auto
       with f obtain x where "s.zero = f x" "x \<in> Field r" unfolding embed_def bij_betw_def
-        using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF r.under_Field] by blast
+        using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF under_Field[of r]] by blast
       with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f"
         unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def
         by (fastforce intro: s.leq_zero_imp)+
@@ -1424,11 +1424,11 @@
         proof safe
           fix h
           assume h_underS: "h \<in> underS (r ^o t) g"
-          hence "h \<in> Field (r ^o t)" unfolding rel.underS_def Field_def by auto
+          hence "h \<in> Field (r ^o t)" unfolding underS_def Field_def by auto
           with fz f_underS have Field_fh: "?f h \<in> Field (s ^o t)"
             unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def
             by (auto elim!: finite_subset[rotated])
-          from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding rel.underS_def by auto
+          from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding underS_def by auto
           with f inj have neq: "?f h \<noteq> ?f g"
             unfolding fun_eq_iff inj_on_def rt.oexp_def Option.map_def FinFunc_def Func_def Let_def
             by simp metis
@@ -1440,7 +1440,7 @@
           with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp"
              using rt.max_fun_diff[OF `h \<noteq> g`] rt.max_fun_diff_in[OF `h \<noteq> g`] unfolding st.Field_oexp
              unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
-          ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding rel.underS_def by auto
+          ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
         qed
         ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
           by blast
@@ -1457,11 +1457,11 @@
   interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
   interpret r!: wo_rel r by unfold_locales (rule r)
   interpret s!: wo_rel s by unfold_locales (rule s)
-  from assms rel.well_order_on_domain[OF r] obtain x where
+  from assms well_order_on_domain[OF r] obtain x where
     x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
-    unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def rel.under_def
+    unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def under_def
     by (auto simp: image_def)
-      (metis equals0D insert_not_empty r.under_def r.zero_in_Field rel.under_empty)
+       (metis (lifting) equals0D mem_Collect_eq r.zero_in_Field singletonI)
   let ?f = "\<lambda>a b. if b \<in> Field s then if b = a then x else r.zero else undefined"
   from x(3) have SUPP: "\<And>y. y \<in> Field s \<Longrightarrow> rs.SUPP (?f y) = {y}" unfolding support_def by auto
   { fix y assume y: "y \<in> Field s"
@@ -1472,7 +1472,7 @@
     proof safe
       fix z
       assume "z \<in> underS s y"
-      hence z: "z \<noteq> y" "(z, y) \<in> s" "z \<in> Field s" unfolding rel.underS_def Field_def by auto
+      hence z: "z \<noteq> y" "(z, y) \<in> s" "z \<in> Field s" unfolding underS_def Field_def by auto
       from x(3) y z(1,3) have "?f z \<noteq> ?f y" unfolding fun_eq_iff by auto
       moreover
       { from x(1,2) have "?f z \<in> FinFunc r s" "?f y \<in> FinFunc r s"
@@ -1484,7 +1484,7 @@
         ultimately have "(?f z, ?f y) \<in> rs.oexp" using y x(1)
           unfolding rs.oexp_def Let_def by auto
       }
-      ultimately show "?f z \<in> underS (r ^o s) (?f y)" unfolding rel.underS_def by blast
+      ultimately show "?f z \<in> underS (r ^o s) (?f y)" unfolding underS_def by blast
     qed
     ultimately have "?f y \<in> Field (r ^o s) \<and> ?f ` underS s y \<subseteq> underS (r ^o s) (?f y)" by blast
   }
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellfounded_More_FP.thy
--- a/src/HOL/Cardinals/Wellfounded_More_FP.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellfounded_More_FP.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -151,7 +151,7 @@
   moreover
   {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
    obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
-   unfolding order_on_defs using Case1 rel.Total_subset_Id by auto
+   unfolding order_on_defs using Case1 Total_subset_Id by auto
    hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
    hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
   }
@@ -169,7 +169,7 @@
       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
       using 1 * unfolding wf_eq_minimal2 by simp
       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
-      using rel.Linear_order_in_diff_Id[of r] ** LI by blast
+      using Linear_order_in_diff_Id[of r] ** LI by blast
       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
     qed
   next
@@ -180,7 +180,7 @@
       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
       using 1 * by simp
       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
-      using rel.Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
+      using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
     qed
   qed
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellorder_Embedding.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -41,7 +41,7 @@
   using EMB unfolding embed_def by simp
   moreover
   {have "under r a \<le> Field r"
-   by (auto simp add: rel.under_Field)
+   by (auto simp add: under_Field)
    hence "\<And> b. b \<in> under r a \<Longrightarrow> f b = g b"
    using EQ by blast
   }
@@ -80,10 +80,10 @@
 proof-
   obtain r where "well_order_on A r" by (fastforce simp add: well_order_on)
   hence 1: "A = Field r \<and> Well_order r"
-  using rel.well_order_on_Well_order by auto
+  using well_order_on_Well_order by auto
   obtain r' where 2: "well_order_on A' r'" by (fastforce simp add: well_order_on)
   hence 2: "A' = Field r' \<and> Well_order r'"
-  using rel.well_order_on_Well_order by auto
+  using well_order_on_Well_order by auto
   hence "(\<exists>f. embed r r' f) \<or> (\<exists>g. embed r' r g)"
   using 1 2 by (auto simp add: wellorders_totally_ordered)
   moreover
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellorder_Embedding_FP.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding_FP.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding_FP.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -40,20 +40,20 @@
 lemma under_underS_bij_betw:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
-        BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
-shows "bij_betw f (rel.under r a) (rel.under r' (f a))"
+        BIJ: "bij_betw f (underS r a) (underS r' (f a))"
+shows "bij_betw f (under r a) (under r' (f a))"
 proof-
-  have "a \<notin> rel.underS r a \<and> f a \<notin> rel.underS r' (f a)"
-  unfolding rel.underS_def by auto
+  have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
+  unfolding underS_def by auto
   moreover
   {have "Refl r \<and> Refl r'" using WELL WELL'
    by (auto simp add: order_on_defs)
-   hence "rel.under r a = rel.underS r a \<union> {a} \<and>
-          rel.under r' (f a) = rel.underS r' (f a) \<union> {f a}"
-   using IN IN' by(auto simp add: rel.Refl_under_underS)
+   hence "under r a = underS r a \<union> {a} \<and>
+          under r' (f a) = underS r' (f a) \<union> {f a}"
+   using IN IN' by(auto simp add: Refl_under_underS)
   }
   ultimately show ?thesis
-  using BIJ notIn_Un_bij_betw[of a "rel.underS r a" f "rel.underS r' (f a)"] by auto
+  using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto
 qed
 
 
@@ -75,7 +75,7 @@
 
 definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
 where
-"embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (rel.under r a) (rel.under r' (f a))"
+"embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
 
 
 lemmas embed_defs = embed_def embed_def[abs_def]
@@ -133,11 +133,11 @@
   using WELL by (auto simp add: wo_rel_def)
   hence 1: "Refl r"
   by (auto simp add: wo_rel.REFL)
-  hence "a \<in> rel.under r a" using IN rel.Refl_under_in by fastforce
-  hence "f a \<in> rel.under r' (f a)"
+  hence "a \<in> under r a" using IN Refl_under_in by fastforce
+  hence "f a \<in> under r' (f a)"
   using EMB IN by (auto simp add: embed_def bij_betw_def)
   thus ?thesis unfolding Field_def
-  by (auto simp: rel.under_def)
+  by (auto simp: under_def)
 qed
 
 
@@ -147,16 +147,16 @@
 shows "embed r r'' (f' o f)"
 proof(unfold embed_def, auto)
   fix a assume *: "a \<in> Field r"
-  hence "bij_betw f (rel.under r a) (rel.under r' (f a))"
+  hence "bij_betw f (under r a) (under r' (f a))"
   using embed_def[of r] EMB by auto
   moreover
   {have "f a \<in> Field r'"
    using EMB WELL * by (auto simp add: embed_in_Field)
-   hence "bij_betw f' (rel.under r' (f a)) (rel.under r'' (f' (f a)))"
+   hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))"
    using embed_def[of r'] EMB' by auto
   }
   ultimately
-  show "bij_betw (f' \<circ> f) (rel.under r a) (rel.under r'' (f'(f a)))"
+  show "bij_betw (f' \<circ> f) (under r a) (under r'' (f'(f a)))"
   by(auto simp add: bij_betw_trans)
 qed
 
@@ -190,14 +190,14 @@
   show ?thesis  using Well' WELL EMB 0 embed_Field[of r r' f]
   proof(unfold wo_rel.ofilter_def, auto simp add: image_def)
     fix a b'
-    assume *: "a \<in> A" and **: "b' \<in> rel.under r' (f a)"
+    assume *: "a \<in> A" and **: "b' \<in> under r' (f a)"
     hence "a \<in> Field r" using 0 by auto
-    hence "bij_betw f (rel.under r a) (rel.under r' (f a))"
+    hence "bij_betw f (under r a) (under r' (f a))"
     using * EMB by (auto simp add: embed_def)
-    hence "f`(rel.under r a) = rel.under r' (f a)"
+    hence "f`(under r a) = under r' (f a)"
     by (simp add: bij_betw_def)
-    with ** image_def[of f "rel.under r a"] obtain b where
-    1: "b \<in> rel.under r a \<and> b' = f b" by blast
+    with ** image_def[of f "under r a"] obtain b where
+    1: "b \<in> under r a \<and> b' = f b" by blast
     hence "b \<in> A" using Well * OF
     by (auto simp add: wo_rel.ofilter_def)
     with 1 show "\<exists>b \<in> A. b' = f b" by blast
@@ -224,14 +224,14 @@
   fix a b
   assume *: "(a,b) \<in> r"
   hence 1: "b \<in> Field r" using Field_def[of r] by blast
-  have "a \<in> rel.under r b"
-  using * rel.under_def[of r] by simp
-  hence "f a \<in> rel.under r' (f b)"
+  have "a \<in> under r b"
+  using * under_def[of r] by simp
+  hence "f a \<in> under r' (f b)"
   using EMB embed_def[of r r' f]
-        bij_betw_def[of f "rel.under r b" "rel.under r' (f b)"]
-        image_def[of f "rel.under r b"] 1 by auto
+        bij_betw_def[of f "under r b" "under r' (f b)"]
+        image_def[of f "under r b"] 1 by auto
   thus "(f a, f b) \<in> r'"
-  by (auto simp add: rel.under_def)
+  by (auto simp add: under_def)
 qed
 
 
@@ -252,16 +252,16 @@
   hence 1: "a \<in> Field r \<and> b \<in> Field r"
   unfolding Field_def by auto
   {assume "(a,b) \<in> r"
-   hence "a \<in> rel.under r b \<and> b \<in> rel.under r b"
-   using Refl by(auto simp add: rel.under_def refl_on_def)
+   hence "a \<in> under r b \<and> b \<in> under r b"
+   using Refl by(auto simp add: under_def refl_on_def)
    hence "a = b"
    using EMB 1 ***
    by (auto simp add: embed_def bij_betw_def inj_on_def)
   }
   moreover
   {assume "(b,a) \<in> r"
-   hence "a \<in> rel.under r a \<and> b \<in> rel.under r a"
-   using Refl by(auto simp add: rel.under_def refl_on_def)
+   hence "a \<in> under r a \<and> b \<in> under r a"
+   using Refl by(auto simp add: under_def refl_on_def)
    hence "a = b"
    using EMB 1 ***
    by (auto simp add: embed_def bij_betw_def inj_on_def)
@@ -275,19 +275,19 @@
 lemma embed_underS:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r r' f" and IN: "a \<in> Field r"
-shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
+shows "bij_betw f (underS r a) (underS r' (f a))"
 proof-
-  have "bij_betw f (rel.under r a) (rel.under r' (f a))"
+  have "bij_betw f (under r a) (under r' (f a))"
   using assms by (auto simp add: embed_def)
   moreover
   {have "f a \<in> Field r'" using assms  embed_Field[of r r' f] by auto
-   hence "rel.under r a = rel.underS r a \<union> {a} \<and>
-          rel.under r' (f a) = rel.underS r' (f a) \<union> {f a}"
-   using assms by (auto simp add: order_on_defs rel.Refl_under_underS)
+   hence "under r a = underS r a \<union> {a} \<and>
+          under r' (f a) = underS r' (f a) \<union> {f a}"
+   using assms by (auto simp add: order_on_defs Refl_under_underS)
   }
   moreover
-  {have "a \<notin> rel.underS r a \<and> f a \<notin> rel.underS r' (f a)"
-   unfolding rel.underS_def by blast
+  {have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
+   unfolding underS_def by blast
   }
   ultimately show ?thesis
   by (auto simp add: notIn_Un_bij_betw3)
@@ -325,20 +325,20 @@
   unfolding Field_def by auto
   have "f a \<in> f`(Field r)"
   using **** by auto
-  hence 2: "rel.under r' (f a) \<le> f`(Field r)"
+  hence 2: "under r' (f a) \<le> f`(Field r)"
   using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce
   (* Main proof *)
-  show "bij_betw f (rel.under r a) (rel.under r' (f a))"
+  show "bij_betw f (under r a) (under r' (f a))"
   proof(unfold bij_betw_def, auto)
-    show  "inj_on f (rel.under r a)"
-    using * by (metis (no_types) rel.under_Field subset_inj_on)
+    show  "inj_on f (under r a)"
+    using * by (metis (no_types) under_Field subset_inj_on)
   next
-    fix b assume "b \<in> rel.under r a"
-    thus "f b \<in> rel.under r' (f a)"
-    unfolding rel.under_def using **
+    fix b assume "b \<in> under r a"
+    thus "f b \<in> under r' (f a)"
+    unfolding under_def using **
     by (auto simp add: compat_def)
   next
-    fix b' assume *****: "b' \<in> rel.under r' (f a)"
+    fix b' assume *****: "b' \<in> under r' (f a)"
     hence "b' \<in> f`(Field r)"
     using 2 by auto
     with Field_def[of r] obtain b where
@@ -349,7 +349,7 @@
        with ** 4 have "(f a, b'): r'"
        by (auto simp add: compat_def)
        with ***** Antisym' have "f a = b'"
-       by(auto simp add: rel.under_def antisym_def)
+       by(auto simp add: under_def antisym_def)
        with 3 **** 4 * have "a = b"
        by(auto simp add: inj_on_def)
       }
@@ -361,15 +361,15 @@
       ultimately
       show ?thesis using Total **** 3 by (fastforce simp add: total_on_def)
     qed
-    with 4 show  "b' \<in> f`(rel.under r a)"
-    unfolding rel.under_def by auto
+    with 4 show  "b' \<in> f`(under r a)"
+    unfolding under_def by auto
   qed
 qed
 
 
 lemma inv_into_ofilter_embed:
 assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
-        BIJ: "\<forall>b \<in> A. bij_betw f (rel.under r b) (rel.under r' (f b))" and
+        BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and
         IMAGE: "f ` A = Field r'"
 shows "embed r' r (inv_into A f)"
 proof-
@@ -390,16 +390,16 @@
     using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
     moreover
     {assume "(b1,b2) \<in> r"
-     hence "b1 \<in> rel.under r b2 \<and> b2 \<in> rel.under r b2"
-     unfolding rel.under_def using 11 Refl
+     hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2"
+     unfolding under_def using 11 Refl
      by (auto simp add: refl_on_def)
      hence "b1 = b2" using BIJ * ** ***
      by (simp add: bij_betw_def inj_on_def)
     }
     moreover
      {assume "(b2,b1) \<in> r"
-     hence "b1 \<in> rel.under r b1 \<and> b2 \<in> rel.under r b1"
-     unfolding rel.under_def using 11 Refl
+     hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1"
+     unfolding under_def using 11 Refl
      by (auto simp add: refl_on_def)
      hence "b1 = b2" using BIJ * ** ***
      by (simp add: bij_betw_def inj_on_def)
@@ -411,20 +411,20 @@
   (*  *)
   let ?f' = "(inv_into A f)"
   (*  *)
-  have 2: "\<forall>b \<in> A. bij_betw ?f' (rel.under r' (f b)) (rel.under r b)"
+  have 2: "\<forall>b \<in> A. bij_betw ?f' (under r' (f b)) (under r b)"
   proof(clarify)
     fix b assume *: "b \<in> A"
-    hence "rel.under r b \<le> A"
+    hence "under r b \<le> A"
     using Well OF by(auto simp add: wo_rel.ofilter_def)
     moreover
-    have "f ` (rel.under r b) = rel.under r' (f b)"
+    have "f ` (under r b) = under r' (f b)"
     using * BIJ by (auto simp add: bij_betw_def)
     ultimately
-    show "bij_betw ?f' (rel.under r' (f b)) (rel.under r b)"
+    show "bij_betw ?f' (under r' (f b)) (under r b)"
     using 1 by (auto simp add: bij_betw_inv_into_subset)
   qed
   (*  *)
-  have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))"
+  have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))"
   proof(clarify)
     fix b' assume *: "b' \<in> Field r'"
     have "b' = f (?f' b')" using * 1
@@ -435,7 +435,7 @@
      with 31 have "?f' b' \<in> A" by auto
     }
     ultimately
-    show  "bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))"
+    show  "bij_betw ?f' (under r' b') (under r (?f' b'))"
     using 2 by auto
   qed
   (*  *)
@@ -445,10 +445,10 @@
 
 lemma inv_into_underS_embed:
 assumes WELL: "Well_order r" and
-        BIJ: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and
+        BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
         IN: "a \<in> Field r" and
-        IMAGE: "f ` (rel.underS r a) = Field r'"
-shows "embed r' r (inv_into (rel.underS r a) f)"
+        IMAGE: "f ` (underS r a) = Field r'"
+shows "embed r' r (inv_into (underS r a) f)"
 using assms
 by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
 
@@ -458,7 +458,7 @@
         IMAGE: "Field r' \<le> f ` (Field r)"
 shows "embed r' r (inv_into (Field r) f)"
 proof-
-  have "(\<forall>b \<in> Field r. bij_betw f (rel.under r b) (rel.under r' (f b)))"
+  have "(\<forall>b \<in> Field r. bij_betw f (under r b) (under r' (f b)))"
   using EMB by (auto simp add: embed_def)
   moreover
   have "f ` (Field r) \<le> Field r'"
@@ -511,101 +511,101 @@
 fixes r ::"'a rel"  and r'::"'a' rel" and
       f :: "'a \<Rightarrow> 'a'" and a::'a
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and
-        IH: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and
-        NOT: "f ` (rel.underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(rel.underS r a))"
-shows "bij_betw f (rel.under r a) (rel.under r' (f a))"
+        IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
+        NOT: "f ` (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))"
+shows "bij_betw f (under r a) (under r' (f a))"
 proof-
   (* Preliminary facts *)
   have Well: "wo_rel r" using WELL unfolding wo_rel_def .
   hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
   have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
-  have OF: "wo_rel.ofilter r (rel.underS r a)"
+  have OF: "wo_rel.ofilter r (underS r a)"
   by (auto simp add: Well wo_rel.underS_ofilter)
-  hence UN: "rel.underS r a = (\<Union>  b \<in> rel.underS r a. rel.under r b)"
-  using Well wo_rel.ofilter_under_UNION[of r "rel.underS r a"] by blast
-  (* Gather facts about elements of rel.underS r a *)
-  {fix b assume *: "b \<in> rel.underS r a"
-   hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding rel.underS_def by auto
+  hence UN: "underS r a = (\<Union>  b \<in> underS r a. under r b)"
+  using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
+  (* Gather facts about elements of underS r a *)
+  {fix b assume *: "b \<in> underS r a"
+   hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
    have t1: "b \<in> Field r"
-   using * rel.underS_Field[of r a] by auto
-   have t2: "f`(rel.under r b) = rel.under r' (f b)"
+   using * underS_Field[of r a] by auto
+   have t2: "f`(under r b) = under r' (f b)"
    using IH * by (auto simp add: bij_betw_def)
-   hence t3: "wo_rel.ofilter r' (f`(rel.under r b))"
+   hence t3: "wo_rel.ofilter r' (f`(under r b))"
    using Well' by (auto simp add: wo_rel.under_ofilter)
-   have "f`(rel.under r b) \<le> Field r'"
-   using t2 by (auto simp add: rel.under_Field)
+   have "f`(under r b) \<le> Field r'"
+   using t2 by (auto simp add: under_Field)
    moreover
-   have "b \<in> rel.under r b"
-   using t1 by(auto simp add: Refl rel.Refl_under_in)
+   have "b \<in> under r b"
+   using t1 by(auto simp add: Refl Refl_under_in)
    ultimately
    have t4:  "f b \<in> Field r'" by auto
-   have "f`(rel.under r b) = rel.under r' (f b) \<and>
-         wo_rel.ofilter r' (f`(rel.under r b)) \<and>
+   have "f`(under r b) = under r' (f b) \<and>
+         wo_rel.ofilter r' (f`(under r b)) \<and>
          f b \<in> Field r'"
    using t2 t3 t4 by auto
   }
   hence bFact:
-  "\<forall>b \<in> rel.underS r a. f`(rel.under r b) = rel.under r' (f b) \<and>
-                       wo_rel.ofilter r' (f`(rel.under r b)) \<and>
+  "\<forall>b \<in> underS r a. f`(under r b) = under r' (f b) \<and>
+                       wo_rel.ofilter r' (f`(under r b)) \<and>
                        f b \<in> Field r'" by blast
   (*  *)
-  have subField: "f`(rel.underS r a) \<le> Field r'"
+  have subField: "f`(underS r a) \<le> Field r'"
   using bFact by blast
   (*  *)
-  have OF': "wo_rel.ofilter r' (f`(rel.underS r a))"
+  have OF': "wo_rel.ofilter r' (f`(underS r a))"
   proof-
-    have "f`(rel.underS r a) = f`(\<Union>  b \<in> rel.underS r a. rel.under r b)"
+    have "f`(underS r a) = f`(\<Union>  b \<in> underS r a. under r b)"
     using UN by auto
-    also have "\<dots> = (\<Union>  b \<in> rel.underS r a. f`(rel.under r b))" by blast
-    also have "\<dots> = (\<Union>  b \<in> rel.underS r a. (rel.under r' (f b)))"
+    also have "\<dots> = (\<Union>  b \<in> underS r a. f`(under r b))" by blast
+    also have "\<dots> = (\<Union>  b \<in> underS r a. (under r' (f b)))"
     using bFact by auto
     finally
-    have "f`(rel.underS r a) = (\<Union>  b \<in> rel.underS r a. (rel.under r' (f b)))" .
+    have "f`(underS r a) = (\<Union>  b \<in> underS r a. (under r' (f b)))" .
     thus ?thesis
     using Well' bFact
-          wo_rel.ofilter_UNION[of r' "rel.underS r a" "\<lambda> b. rel.under r' (f b)"] by fastforce
+          wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
   qed
   (*  *)
-  have "f`(rel.underS r a) \<union> rel.AboveS r' (f`(rel.underS r a)) = Field r'"
+  have "f`(underS r a) \<union> AboveS r' (f`(underS r a)) = Field r'"
   using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)
-  hence NE: "rel.AboveS r' (f`(rel.underS r a)) \<noteq> {}"
+  hence NE: "AboveS r' (f`(underS r a)) \<noteq> {}"
   using subField NOT by blast
   (* Main proof *)
-  have INCL1: "f`(rel.underS r a) \<le> rel.underS r' (f a) "
+  have INCL1: "f`(underS r a) \<le> underS r' (f a) "
   proof(auto)
-    fix b assume *: "b \<in> rel.underS r a"
+    fix b assume *: "b \<in> underS r a"
     have "f b \<noteq> f a \<and> (f b, f a) \<in> r'"
     using subField Well' SUC NE *
-          wo_rel.suc_greater[of r' "f`(rel.underS r a)" "f b"] by force
-    thus "f b \<in> rel.underS r' (f a)"
-    unfolding rel.underS_def by simp
+          wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force
+    thus "f b \<in> underS r' (f a)"
+    unfolding underS_def by simp
   qed
   (*  *)
-  have INCL2: "rel.underS r' (f a) \<le> f`(rel.underS r a)"
+  have INCL2: "underS r' (f a) \<le> f`(underS r a)"
   proof
-    fix b' assume "b' \<in> rel.underS r' (f a)"
+    fix b' assume "b' \<in> underS r' (f a)"
     hence "b' \<noteq> f a \<and> (b', f a) \<in> r'"
-    unfolding rel.underS_def by simp
-    thus "b' \<in> f`(rel.underS r a)"
+    unfolding underS_def by simp
+    thus "b' \<in> f`(underS r a)"
     using Well' SUC NE OF'
-          wo_rel.suc_ofilter_in[of r' "f ` rel.underS r a" b'] by auto
+          wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto
   qed
   (*  *)
-  have INJ: "inj_on f (rel.underS r a)"
+  have INJ: "inj_on f (underS r a)"
   proof-
-    have "\<forall>b \<in> rel.underS r a. inj_on f (rel.under r b)"
+    have "\<forall>b \<in> underS r a. inj_on f (under r b)"
     using IH by (auto simp add: bij_betw_def)
     moreover
-    have "\<forall>b. wo_rel.ofilter r (rel.under r b)"
+    have "\<forall>b. wo_rel.ofilter r (under r b)"
     using Well by (auto simp add: wo_rel.under_ofilter)
     ultimately show  ?thesis
     using WELL bFact UN
-          UNION_inj_on_ofilter[of r "rel.underS r a" "\<lambda>b. rel.under r b" f]
+          UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f]
     by auto
   qed
   (*  *)
-  have BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
+  have BIJ: "bij_betw f (underS r a) (underS r' (f a))"
   unfolding bij_betw_def
   using INJ INCL1 INCL2 by auto
   (*  *)
@@ -622,14 +622,14 @@
       f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool"  and a::'a
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
 MAIN1:
-  "\<And> a. (False \<notin> g`(rel.underS r a) \<and> f`(rel.underS r a) \<noteq> Field r'
-          \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True)
+  "\<And> a. (False \<notin> g`(underS r a) \<and> f`(underS r a) \<noteq> Field r'
+          \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True)
          \<and>
-         (\<not>(False \<notin> (g`(rel.underS r a)) \<and> f`(rel.underS r a) \<noteq> Field r')
+         (\<not>(False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')
           \<longrightarrow> g a = False)" and
-MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(rel.under r a) \<longrightarrow>
-              bij_betw f (rel.under r a) (rel.under r' (f a))" and
-Case: "a \<in> Field r \<and> False \<in> g`(rel.under r a)"
+MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
+              bij_betw f (under r a) (under r' (f a))" and
+Case: "a \<in> Field r \<and> False \<in> g`(under r a)"
 shows "\<exists>f'. embed r' r f'"
 proof-
   have Well: "wo_rel r" using WELL unfolding wo_rel_def .
@@ -638,13 +638,13 @@
   have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto
   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
   (*  *)
-  have 0: "rel.under r a = rel.underS r a \<union> {a}"
-  using Refl Case by(auto simp add: rel.Refl_under_underS)
+  have 0: "under r a = underS r a \<union> {a}"
+  using Refl Case by(auto simp add: Refl_under_underS)
   (*  *)
   have 1: "g a = False"
   proof-
     {assume "g a \<noteq> False"
-     with 0 Case have "False \<in> g`(rel.underS r a)" by blast
+     with 0 Case have "False \<in> g`(underS r a)" by blast
      with MAIN1 have "g a = False" by blast}
     thus ?thesis by blast
   qed
@@ -653,12 +653,12 @@
   (*  *)
   have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast
   (*  *)
-  have 3: "False \<notin> g`(rel.underS r ?a)"
+  have 3: "False \<notin> g`(underS r ?a)"
   proof
-    assume "False \<in> g`(rel.underS r ?a)"
-    then obtain b where "b \<in> rel.underS r ?a" and 31: "g b = False" by auto
+    assume "False \<in> g`(underS r ?a)"
+    then obtain b where "b \<in> underS r ?a" and 31: "g b = False" by auto
     hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a"
-    by (auto simp add: rel.underS_def)
+    by (auto simp add: underS_def)
     hence "b \<in> Field r" unfolding Field_def by auto
     with 31 have "b \<in> ?A" by auto
     hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce
@@ -672,25 +672,25 @@
   (*   *)
   have 5: "g ?a = False" using temp by blast
   (*  *)
-  have 6: "f`(rel.underS r ?a) = Field r'"
+  have 6: "f`(underS r ?a) = Field r'"
   using MAIN1[of ?a] 3 5 by blast
   (*  *)
-  have 7: "\<forall>b \<in> rel.underS r ?a. bij_betw f (rel.under r b) (rel.under r' (f b))"
+  have 7: "\<forall>b \<in> underS r ?a. bij_betw f (under r b) (under r' (f b))"
   proof
-    fix b assume as: "b \<in> rel.underS r ?a"
+    fix b assume as: "b \<in> underS r ?a"
     moreover
-    have "wo_rel.ofilter r (rel.underS r ?a)"
+    have "wo_rel.ofilter r (underS r ?a)"
     using Well by (auto simp add: wo_rel.underS_ofilter)
     ultimately
-    have "False \<notin> g`(rel.under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
+    have "False \<notin> g`(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
     moreover have "b \<in> Field r"
-    unfolding Field_def using as by (auto simp add: rel.underS_def)
+    unfolding Field_def using as by (auto simp add: underS_def)
     ultimately
-    show "bij_betw f (rel.under r b) (rel.under r' (f b))"
+    show "bij_betw f (under r b) (under r' (f b))"
     using MAIN2 by auto
   qed
   (*  *)
-  have "embed r' r (inv_into (rel.underS r ?a) f)"
+  have "embed r' r (inv_into (underS r ?a) f)"
   using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto
   thus ?thesis
   unfolding embed_def by blast
@@ -709,18 +709,18 @@
   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
   (* Main proof *)
   obtain H where H_def: "H =
-  (\<lambda>h a. if False \<notin> (snd o h)`(rel.underS r a) \<and> (fst o h)`(rel.underS r a) \<noteq> Field r'
-                then (wo_rel.suc r' ((fst o h)`(rel.underS r a)), True)
+  (\<lambda>h a. if False \<notin> (snd o h)`(underS r a) \<and> (fst o h)`(underS r a) \<noteq> Field r'
+                then (wo_rel.suc r' ((fst o h)`(underS r a)), True)
                 else (undefined, False))" by blast
   have Adm: "wo_rel.adm_wo r H"
   using Well
   proof(unfold wo_rel.adm_wo_def, clarify)
     fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x
-    assume "\<forall>y\<in>rel.underS r x. h1 y = h2 y"
-    hence "\<forall>y\<in>rel.underS r x. (fst o h1) y = (fst o h2) y \<and>
+    assume "\<forall>y\<in>underS r x. h1 y = h2 y"
+    hence "\<forall>y\<in>underS r x. (fst o h1) y = (fst o h2) y \<and>
                           (snd o h1) y = (snd o h2) y" by auto
-    hence "(fst o h1)`(rel.underS r x) = (fst o h2)`(rel.underS r x) \<and>
-           (snd o h1)`(rel.underS r x) = (snd o h2)`(rel.underS r x)"
+    hence "(fst o h1)`(underS r x) = (fst o h2)`(underS r x) \<and>
+           (snd o h1)`(underS r x) = (snd o h2)`(underS r x)"
       by (auto simp add: image_def)
     thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
   qed
@@ -729,21 +729,21 @@
   where h_def: "h = wo_rel.worec r H" and
         f_def: "f = fst o h" and g_def: "g = snd o h" by blast
   obtain test where test_def:
-  "test = (\<lambda> a. False \<notin> (g`(rel.underS r a)) \<and> f`(rel.underS r a) \<noteq> Field r')" by blast
+  "test = (\<lambda> a. False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')" by blast
   (*  *)
   have *: "\<And> a. h a  = H h a"
   using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def)
   have Main1:
-  "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True) \<and>
+  "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
          (\<not>(test a) \<longrightarrow> g a = False)"
   proof-  (* How can I prove this withou fixing a? *)
-    fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True) \<and>
+    fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
                 (\<not>(test a) \<longrightarrow> g a = False)"
     using *[of a] test_def f_def g_def H_def by auto
   qed
   (*  *)
-  let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(rel.under r a) \<longrightarrow>
-                   bij_betw f (rel.under r a) (rel.under r' (f a))"
+  let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
+                   bij_betw f (under r a) (under r' (f a))"
   have Main2: "\<And> a. ?phi a"
   proof-
     fix a show "?phi a"
@@ -752,46 +752,46 @@
       fix a
       assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and
              *: "a \<in> Field r" and
-             **: "False \<notin> g`(rel.under r a)"
-      have 1: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))"
+             **: "False \<notin> g`(under r a)"
+      have 1: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))"
       proof(clarify)
-        fix b assume ***: "b \<in> rel.underS r a"
-        hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding rel.underS_def by auto
+        fix b assume ***: "b \<in> underS r a"
+        hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
         moreover have "b \<in> Field r"
-        using *** rel.underS_Field[of r a] by auto
-        moreover have "False \<notin> g`(rel.under r b)"
-        using 0 ** Trans rel.under_incr[of r b a] by auto
-        ultimately show "bij_betw f (rel.under r b) (rel.under r' (f b))"
+        using *** underS_Field[of r a] by auto
+        moreover have "False \<notin> g`(under r b)"
+        using 0 ** Trans under_incr[of r b a] by auto
+        ultimately show "bij_betw f (under r b) (under r' (f b))"
         using IH by auto
       qed
       (*  *)
-      have 21: "False \<notin> g`(rel.underS r a)"
-      using ** rel.underS_subset_under[of r a] by auto
-      have 22: "g`(rel.under r a) \<le> {True}" using ** by auto
-      moreover have 23: "a \<in> rel.under r a"
-      using Refl * by (auto simp add: rel.Refl_under_in)
+      have 21: "False \<notin> g`(underS r a)"
+      using ** underS_subset_under[of r a] by auto
+      have 22: "g`(under r a) \<le> {True}" using ** by auto
+      moreover have 23: "a \<in> under r a"
+      using Refl * by (auto simp add: Refl_under_in)
       ultimately have 24: "g a = True" by blast
-      have 2: "f`(rel.underS r a) \<noteq> Field r'"
+      have 2: "f`(underS r a) \<noteq> Field r'"
       proof
-        assume "f`(rel.underS r a) = Field r'"
+        assume "f`(underS r a) = Field r'"
         hence "g a = False" using Main1 test_def by blast
         with 24 show False using ** by blast
       qed
       (*  *)
-      have 3: "f a = wo_rel.suc r' (f`(rel.underS r a))"
+      have 3: "f a = wo_rel.suc r' (f`(underS r a))"
       using 21 2 Main1 test_def by blast
       (*  *)
-      show "bij_betw f (rel.under r a) (rel.under r' (f a))"
+      show "bij_betw f (under r a) (under r' (f a))"
       using WELL  WELL' 1 2 3 *
             wellorders_totally_ordered_aux[of r r' a f] by auto
     qed
   qed
   (*  *)
-  let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(rel.under r a))"
+  let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(under r a))"
   show ?thesis
   proof(cases "\<exists>a. ?chi a")
     assume "\<not> (\<exists>a. ?chi a)"
-    hence "\<forall>a \<in> Field r.  bij_betw f (rel.under r a) (rel.under r' (f a))"
+    hence "\<forall>a \<in> Field r.  bij_betw f (under r a) (under r' (f a))"
     using Main2 by blast
     thus ?thesis unfolding embed_def by blast
   next
@@ -817,16 +817,16 @@
 lemma embed_determined:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r r' f" and IN: "a \<in> Field r"
-shows "f a = wo_rel.suc r' (f`(rel.underS r a))"
+shows "f a = wo_rel.suc r' (f`(underS r a))"
 proof-
-  have "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
+  have "bij_betw f (underS r a) (underS r' (f a))"
   using assms by (auto simp add: embed_underS)
-  hence "f`(rel.underS r a) = rel.underS r' (f a)"
+  hence "f`(underS r a) = underS r' (f a)"
   by (auto simp add: bij_betw_def)
   moreover
   {have "f a \<in> Field r'" using IN
    using EMB WELL embed_Field[of r r' f] by auto
-   hence "f a = wo_rel.suc r' (rel.underS r' (f a))"
+   hence "f a = wo_rel.suc r' (underS r' (f a))"
    using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)
   }
   ultimately show ?thesis by simp
@@ -841,9 +841,9 @@
   fix a
   assume IH: "\<forall>b. b \<noteq> a \<and> (b,a): r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and
          *: "a \<in> Field r"
-  hence "\<forall>b \<in> rel.underS r a. f b = g b"
-  unfolding rel.underS_def by (auto simp add: Field_def)
-  hence "f`(rel.underS r a) = g`(rel.underS r a)" by force
+  hence "\<forall>b \<in> underS r a. f b = g b"
+  unfolding underS_def by (auto simp add: Field_def)
+  hence "f`(underS r a) = g`(underS r a)" by force
   thus "f a = g a"
   using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
 qed
@@ -1083,28 +1083,28 @@
 next
   assume *: "bij_betw f (Field r) (Field r')" and
          **: "\<forall>a\<in>Field r. \<forall>b\<in>Field r. ((a, b) \<in> r) = ((f a, f b) \<in> r')"
-  have 1: "\<And> a. rel.under r a \<le> Field r \<and> rel.under r' (f a) \<le> Field r'"
-  by (auto simp add: rel.under_Field)
+  have 1: "\<And> a. under r a \<le> Field r \<and> under r' (f a) \<le> Field r'"
+  by (auto simp add: under_Field)
   have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def)
   {fix a assume ***: "a \<in> Field r"
-   have "bij_betw f (rel.under r a) (rel.under r' (f a))"
+   have "bij_betw f (under r a) (under r' (f a))"
    proof(unfold bij_betw_def, auto)
-     show "inj_on f (rel.under r a)"
+     show "inj_on f (under r a)"
      using 1 2 by (metis subset_inj_on)
    next
-     fix b assume "b \<in> rel.under r a"
+     fix b assume "b \<in> under r a"
      hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
-     unfolding rel.under_def by (auto simp add: Field_def Range_def Domain_def)
-     with 1 ** show "f b \<in> rel.under r' (f a)"
-     unfolding rel.under_def by auto
+     unfolding under_def by (auto simp add: Field_def Range_def Domain_def)
+     with 1 ** show "f b \<in> under r' (f a)"
+     unfolding under_def by auto
    next
-     fix b' assume "b' \<in> rel.under r' (f a)"
-     hence 3: "(b',f a) \<in> r'" unfolding rel.under_def by simp
+     fix b' assume "b' \<in> under r' (f a)"
+     hence 3: "(b',f a) \<in> r'" unfolding under_def by simp
      hence "b' \<in> Field r'" unfolding Field_def by auto
      with * obtain b where "b \<in> Field r \<and> f b = b'"
      unfolding bij_betw_def by force
      with 3 ** ***
-     show "b' \<in> f ` (rel.under r a)" unfolding rel.under_def by blast
+     show "b' \<in> f ` (under r a)" unfolding under_def by blast
    qed
   }
   thus "embed r r' f" unfolding embed_def using * by auto
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellorder_Extension.thy
--- a/src/HOL/Cardinals/Wellorder_Extension.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Extension.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -178,7 +178,7 @@
     where "p \<subseteq> w" and wo: "Well_order w" by blast
   let ?A = "UNIV - Field w"
   from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" ..
-  have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp
+  have [simp]: "Field w' = ?A" using well_order_on_Well_order [OF wo'] by simp
   have *: "Field w \<inter> Field w' = {}" by simp
   let ?w = "w \<union>o w'"
   have "p \<subseteq> ?w" using `p \<subseteq> w` by (auto simp: Osum_def)
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellorder_Relation.thy
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -37,7 +37,7 @@
 proof-
   have "adm_wf (r - Id) H"
   unfolding adm_wf_def
-  using ADM adm_wo_def[of H] underS_def by auto
+  using ADM adm_wo_def[of H] underS_def[of r] by auto
   hence "f = wfrec (r - Id) H"
   using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
   thus ?thesis unfolding worec_def .
@@ -97,7 +97,7 @@
   have "Under A \<le> under (minim A)"
   proof
     fix x assume "x \<in> Under A"
-    with 1 Under_def have "(x,minim A) \<in> r" by auto
+    with 1 Under_def[of r] have "(x,minim A) \<in> r" by auto
     thus "x \<in> under(minim A)" unfolding under_def by simp
   qed
   (*  *)
@@ -133,7 +133,7 @@
   have "UnderS A \<le> underS (minim A)"
   proof
     fix x assume "x \<in> UnderS A"
-    with 1 UnderS_def have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto
+    with 1 UnderS_def[of r] have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto
     thus "x \<in> underS(minim A)" unfolding underS_def by simp
   qed
   (*  *)
@@ -173,7 +173,7 @@
 shows "supr B \<in> Above B"
 proof(unfold supr_def)
   have "Above B \<le> Field r"
-  using Above_Field by auto
+  using Above_Field[of r] by auto
   thus "minim (Above B) \<in> Above B"
   using assms by (simp add: minim_in)
 qed
@@ -185,7 +185,7 @@
 proof-
   from assms supr_Above
   have "supr B \<in> Above B" by simp
-  with IN Above_def show ?thesis by simp
+  with IN Above_def[of r] show ?thesis by simp
 qed
 
 lemma supr_least_Above:
@@ -194,7 +194,7 @@
 shows "(supr B, a) \<in> r"
 proof(unfold supr_def)
   have "Above B \<le> Field r"
-  using Above_Field by auto
+  using Above_Field[of r] by auto
   thus "(minim (Above B), a) \<in> r"
   using assms minim_least
   by simp
@@ -211,7 +211,7 @@
 shows "a = supr B"
 proof(unfold supr_def)
   have "Above B \<le> Field r"
-  using Above_Field by auto
+  using Above_Field[of r] by auto
   thus "a = minim (Above B)"
   using assms equals_minim by simp
 qed
@@ -236,7 +236,7 @@
 shows "supr B \<in> Field r"
 proof-
   have "supr B \<in> Above B" using supr_Above assms by simp
-  thus ?thesis using assms Above_Field by auto
+  thus ?thesis using assms Above_Field[of r] by auto
 qed
 
 lemma supr_above_Above:
@@ -264,13 +264,13 @@
 shows "a = supr (under a)"
 proof-
   have "under a \<le> Field r"
-  using under_Field by auto
+  using under_Field[of r] by auto
   moreover
   have "under a \<noteq> {}"
-  using IN Refl_under_in REFL by auto
+  using IN Refl_under_in[of r] REFL by auto
   moreover
   have "a \<in> Above (under a)"
-  using in_Above_under IN by auto
+  using in_Above_under[of _ r] IN by auto
   moreover
   have "\<forall>a' \<in> Above (under a). (a,a') \<in> r"
   proof(unfold Above_def under_def, auto)
@@ -347,7 +347,7 @@
 shows "a' = a \<or> (a',a) \<in> r"
 proof-
   have *: "suc {a} \<in> Field r \<and> a' \<in> Field r"
-  using WELL REL well_order_on_domain by auto
+  using WELL REL well_order_on_domain by metis
   {assume **: "a' \<noteq> a"
    hence "(a,a') \<in> r \<or> (a',a) \<in> r"
    using TOTAL IN * by (auto simp add: total_on_def)
@@ -369,7 +369,7 @@
 shows "underS (suc {a}) = under a"
 proof-
   have 1: "AboveS {a} \<noteq> {}"
-  using ABV aboveS_AboveS_singl by auto
+  using ABV aboveS_AboveS_singl[of r] by auto
   have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r"
   using suc_greater[of "{a}" a] IN 1 by auto
   (*   *)
@@ -408,12 +408,12 @@
 proof(unfold ofilter_def, auto)
   fix x assume "x \<in> Under A"
   thus "x \<in> Field r"
-  using Under_Field assms by auto
+  using Under_Field[of r] 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
+  using TRANS under_Under_trans[of r] by auto
 qed
 
 lemma ofilter_UnderS[simp]:
@@ -422,12 +422,12 @@
 proof(unfold ofilter_def, auto)
   fix x assume "x \<in> UnderS A"
   thus "x \<in> Field r"
-  using UnderS_Field assms by auto
+  using UnderS_Field[of r] 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
+  using TRANS ANTISYM under_UnderS_trans[of r] by auto
 qed
 
 lemma ofilter_Int[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)"
@@ -469,7 +469,7 @@
   (* Main proof *)
   fix x assume "x \<in> Under(Under A)"
   with 1 have 1: "(x,minim A) \<in> r"
-  using Under_def by auto
+  using Under_def[of r] by auto
   with Field_def have "x \<in> Field r" by fastforce
   moreover
   {fix y assume *: "y \<in> A"
@@ -506,7 +506,7 @@
     hence "(suc A,x) \<in> r"
     using suc_least_AboveS by auto
     moreover
-    have "(x,suc A) \<in> r" using * under_def by auto
+    have "(x,suc A) \<in> r" using * under_def[of r] by auto
     ultimately show "x = suc A"
     using ANTISYM antisym_def[of r] by auto
   qed
diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellorder_Relation_FP.thy
--- a/src/HOL/Cardinals/Wellorder_Relation_FP.thy	Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation_FP.thy	Thu Jan 16 20:52:54 2014 +0100
@@ -18,7 +18,9 @@
 i.e., as containing the diagonals of their fields. *}
 
 
-locale wo_rel = rel + assumes WELL: "Well_order r"
+locale wo_rel =
+  fixes r :: "'a rel"
+  assumes WELL: "Well_order r"
 begin
 
 text{* The following context encompasses all this section. In other words,
@@ -26,6 +28,15 @@
 
 (* context wo_rel  *)
 
+abbreviation under where "under \<equiv> Order_Relation_More_FP.under r"
+abbreviation underS where "underS \<equiv> Order_Relation_More_FP.underS r"
+abbreviation Under where "Under \<equiv> Order_Relation_More_FP.Under r"
+abbreviation UnderS where "UnderS \<equiv> Order_Relation_More_FP.UnderS r"
+abbreviation above where "above \<equiv> Order_Relation_More_FP.above r"
+abbreviation aboveS where "aboveS \<equiv> Order_Relation_More_FP.aboveS r"
+abbreviation Above where "Above \<equiv> Order_Relation_More_FP.Above r"
+abbreviation AboveS where "AboveS \<equiv> Order_Relation_More_FP.AboveS r"
+
 
 subsection {* Auxiliaries *}
 
@@ -109,7 +120,7 @@
   let ?rS = "r - Id"
   have "adm_wf (r - Id) H"
   unfolding adm_wf_def
-  using ADM adm_wo_def[of H] underS_def by auto
+  using ADM adm_wo_def[of H] underS_def[of r] by auto
   hence "wfrec ?rS H = H (wfrec ?rS H)"
   using WF wfrec_fixpoint[of ?rS H] by simp
   thus ?thesis unfolding worec_def .
@@ -327,7 +338,7 @@
 shows "suc B \<in> AboveS B"
 proof(unfold suc_def)
   have "AboveS B \<le> Field r"
-  using AboveS_Field by auto
+  using AboveS_Field[of r] by auto
   thus "minim (AboveS B) \<in> AboveS B"
   using assms by (simp add: minim_in)
 qed
@@ -340,7 +351,7 @@
 proof-
   from assms suc_AboveS
   have "suc B \<in> AboveS B" by simp
-  with IN AboveS_def show ?thesis by simp
+  with IN AboveS_def[of r] show ?thesis by simp
 qed
 
 
@@ -349,7 +360,7 @@
 shows "(suc B,a) \<in> r"
 proof(unfold suc_def)
   have "AboveS B \<le> Field r"
-  using AboveS_Field by auto
+  using AboveS_Field[of r] by auto
   thus "(minim (AboveS B),a) \<in> r"
   using assms minim_least by simp
 qed
@@ -361,7 +372,7 @@
 proof-
   have "suc B \<in> AboveS B" using suc_AboveS assms by simp
   thus ?thesis
-  using assms AboveS_Field by auto
+  using assms AboveS_Field[of r] by auto
 qed
 
 
@@ -371,7 +382,7 @@
 shows "a = suc B"
 proof(unfold suc_def)
   have "AboveS B \<le> Field r"
-  using AboveS_Field[of B] by auto
+  using AboveS_Field[of r B] by auto
   thus "a = minim (AboveS B)"
   using assms equals_minim
   by simp
@@ -383,17 +394,17 @@
 shows "a = suc (underS a)"
 proof-
   have "underS a \<le> Field r"
-  using underS_Field by auto
+  using underS_Field[of r] by auto
   moreover
   have "a \<in> AboveS (underS a)"
-  using in_AboveS_underS IN by auto
+  using in_AboveS_underS IN by fast
   moreover
   have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
   proof(clarify)
     fix a'
     assume *: "a' \<in> AboveS (underS a)"
     hence **: "a' \<in> Field r"
-    using AboveS_Field by auto
+    using AboveS_Field by fast
     {assume "(a,a') \<notin> r"
      hence "a' = a \<or> (a',a) \<in> r"
      using TOTAL IN ** by (auto simp add: total_on_def)
@@ -407,7 +418,7 @@
       hence "a' \<in> underS a"
       unfolding underS_def by simp
       hence "a' \<notin> AboveS (underS a)"
-      using AboveS_disjoint by blast
+      using AboveS_disjoint by fast
       with * have False by simp
      }
      ultimately have "(a,a') \<in> r" by blast
@@ -486,7 +497,7 @@
          hence "(?a,x) \<in> r"
          using TOTAL total_on_def[of "Field r" r]
                2 4 11 12 by auto
-         hence "?a \<in> under x" using under_def by auto
+         hence "?a \<in> under x" using under_def[of r] by auto
          hence "?a \<in> A" using ** 13 by blast
          with 4 have False by simp
         }
@@ -527,7 +538,7 @@
   thus "(\<Union> a \<in> A. under a) \<le> A" by blast
 next
   have "\<forall>a \<in> A. a \<in> under a"
-  using REFL Refl_under_in assms ofilter_def by blast
+  using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
   thus "A \<le> (\<Union> a \<in> A. under a)" by blast
 qed
 
@@ -562,13 +573,13 @@
     }
     moreover
     {assume "(a,b) \<in> r"
-     with underS_incr TRANS ANTISYM 1 2
+     with underS_incr[of r] TRANS ANTISYM 1 2
      have "A \<le> B" by auto
      hence ?thesis by auto
     }
     moreover
      {assume "(b,a) \<in> r"
-     with underS_incr TRANS ANTISYM 1 2
+     with underS_incr[of r] TRANS ANTISYM 1 2
      have "B \<le> A" by auto
      hence ?thesis by auto
     }
@@ -582,7 +593,7 @@
 shows "A \<union> (AboveS A) = Field r"
 proof
   show "A \<union> (AboveS A) \<le> Field r"
-  using assms ofilter_def AboveS_Field by auto
+  using assms ofilter_def AboveS_Field[of r] by auto
 next
   {fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
    {fix y assume ***: "y \<in> A"
@@ -592,7 +603,7 @@
      have "y \<in> Field r" using assms ofilter_def *** by auto
      ultimately have "(x,y) \<in> r"
      using 1 * TOTAL total_on_def[of _ r] by auto
-     with *** assms ofilter_def under_def have "x \<in> A" by auto
+     with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
      with ** have False by contradiction
     }
     hence "(y,x) \<in> r" by blast
@@ -610,7 +621,7 @@
 shows "b \<in> A"
 proof-
   have *: "suc A \<in> Field r \<and> b \<in> Field r"
-  using WELL REL well_order_on_domain by auto
+  using WELL REL well_order_on_domain[of "Field r"] by auto
   {assume **: "b \<notin> A"
    hence "b \<in> AboveS A"
    using OF * ofilter_AboveS_Field by auto