# HG changeset patch
# User traytel
# Date 1366814599 -7200
# Node ID 67f05cb13e08545facc3bf433646592bd9f284a6
# Parent  0051318acc9dba243625822005fc3a92ef58145e
optimized proofs

diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -86,7 +86,7 @@
 proof-
   let ?Y = "{y. EX x. (x,y) : R}"  let ?X = "{x. EX y. (x,y) : R}"
   let ?f = "% y. SOME x. (x,y) : R"
-  have "?f ` ?Y <= ?X" using someI by force (* FIXME: takes a bit long *)
+  have "?f ` ?Y <= ?X" by (auto dest: someI)
   moreover have "inj_on ?f ?Y"
   unfolding inj_on_def proof(auto)
     fix y1 x1 y2 x2
@@ -603,7 +603,7 @@
 shows "|{a} Un A| <o |B|"
 proof-
   have "|{a}| <o |B|" using assms by auto
-  thus ?thesis using assms card_of_Un_ordLess_infinite[of B] by fastforce
+  thus ?thesis using assms card_of_Un_ordLess_infinite[of B] by blast
 qed
 
 lemma card_of_Un_singl_ordLess_infinite:
@@ -612,7 +612,7 @@
 using assms card_of_Un_singl_ordLess_infinite1[of B A]
 proof(auto)
   assume "|insert a A| <o |B|"
-  moreover have "|A| <=o |insert a A|" using card_of_mono1[of A] by blast
+  moreover have "|A| <=o |insert a A|" using card_of_mono1[of A "insert a A"] by blast
   ultimately show "|A| <o |B|" using ordLeq_ordLess_trans by blast
 qed
 
diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -580,7 +580,7 @@
     qed
   qed
   hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"
-  unfolding bij_betw_def inj_on_def f_def by auto
+  unfolding bij_betw_def inj_on_def f_def by force
   thus ?thesis using card_of_ordIso by blast
 qed
 
@@ -836,7 +836,7 @@
   have "\<forall>i. i \<in> I \<longrightarrow> (\<exists>f. inj_on f (A i) \<and> f ` (A i) \<le> B i)"
   using assms by (auto simp add: card_of_ordLeq)
   with choice[of "\<lambda> i f. i \<in> I \<longrightarrow> inj_on f (A i) \<and> f ` (A i) \<le> B i"]
-  obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i) ` (A i) \<le> B i" by fastforce
+  obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i) ` (A i) \<le> B i" by metis
   obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast
   have "inj_on g (Sigma I A) \<and> g ` (Sigma I A) \<le> (Sigma I B)"
   using 1 unfolding inj_on_def using g_def by force
@@ -1766,9 +1766,9 @@
 proof
   assume "natLeq_on m \<le>o natLeq_on n"
   then obtain f where "inj_on f {0..<m} \<and> f ` {0..<m} \<le> {0..<n}"
-  using Field_natLeq_on[of m] Field_natLeq_on[of n]
-  unfolding ordLeq_def using embed_inj_on[of "natLeq_on m"  "natLeq_on n"]
-  embed_Field[of "natLeq_on m" "natLeq_on n"] using natLeq_on_Well_order[of m] by fastforce
+  unfolding ordLeq_def using
+    embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
+     embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
   thus "m \<le> n" using atLeastLessThan_less_eq2 by blast
 next
   assume "m \<le> n"
@@ -2238,7 +2238,7 @@
     proof (cases "(a,b) \<in> A <*> B")
       case False
       thus ?thesis using assms unfolding Func_def
-      apply(cases "f1 (a,b)") apply(cases "f2 (a,b)", fastforce, fastforce)
+      apply(cases "f1 (a,b)") apply(cases "f2 (a,b)", simp, blast)
       apply(cases "f2 (a,b)") by auto
     next
       case True hence a: "a \<in> A" and b: "b \<in> B" by auto
@@ -2406,7 +2406,7 @@
   qed
   moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
   using inv_into_into j2A2 B1 A2 inv_into_into
-  unfolding j1_def image_def by(force, force)
+  unfolding j1_def image_def by fast+
   ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
   unfolding Func_map_def[abs_def] unfolding image_def by auto
 qed(insert B1 Func_map[OF _ _ A2(2)], auto)
diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Constructions_on_Wellorders.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -44,7 +44,7 @@
 
 lemma wf_Restr:
 "wf r \<Longrightarrow> wf(Restr r A)"
-using wf_subset Restr_subset by blast
+using Restr_subset by (elim wf_subset) simp
 
 lemma Restr_incr1:
 "A \<le> B \<Longrightarrow> Restr r A \<le> Restr r B"
@@ -384,7 +384,7 @@
     assume Case1: "B \<noteq> {}"
     hence "B \<noteq> {} \<and> B \<le> Field r" using B_def by auto
     then obtain a where 1: "a \<in> B" and 2: "\<forall>a1 \<in> B. (a1,a) \<notin> r"
-    using WF  unfolding wf_eq_minimal2 by blast
+    using WF  unfolding wf_eq_minimal2 by metis
     hence 3: "a \<in> Field r \<and> a \<notin> Field r'" using B_def FLD by auto
     (*  *)
     have "\<forall>a1 \<in> A. (a1,a) \<notin> r Osum r'"
@@ -412,7 +412,7 @@
     assume Case2: "B = {}"
     hence 1: "A \<noteq> {} \<and> A \<le> Field r'" using * ** B_def by auto
     then obtain a' where 2: "a' \<in> A" and 3: "\<forall>a1' \<in> A. (a1',a') \<notin> r'"
-    using WF' unfolding wf_eq_minimal2 by blast
+    using WF' unfolding wf_eq_minimal2 by metis
     hence 4: "a' \<in> Field r' \<and> a' \<notin> Field r" using 1 FLD by blast
     (*  *)
     have "\<forall>a1' \<in> A. (a1',a') \<notin> r Osum r'"
@@ -450,15 +450,14 @@
   thus ?thesis by(auto simp add: Osum_def)
 qed
 
-
 lemma wf_Int_Times:
 assumes "A Int B = {}"
 shows "wf(A \<times> B)"
-proof(unfold wf_def, auto)
+proof(unfold wf_def mem_Sigma_iff, intro impI allI)
   fix P x
   assume *: "\<forall>x. (\<forall>y. y \<in> A \<and> x \<in> B \<longrightarrow> P y) \<longrightarrow> P x"
   moreover have "\<forall>y \<in> A. P y" using assms * by blast
-  ultimately show "P x" using * by (case_tac "x \<in> B", auto)
+  ultimately show "P x" using * by (case_tac "x \<in> B") blast+
 qed
 
 lemma Osum_minus_Id1:
diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Constructions_on_Wellorders_Base.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders_Base.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders_Base.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -879,7 +879,7 @@
   {assume "r' \<le>o r"
    then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
    unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
-   hence False using finite_imageD finite_subset FIN INF by blast
+   hence False using finite_imageD finite_subset FIN INF by metis
   }
   thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
 qed
@@ -1092,7 +1092,7 @@
   have "A \<noteq> {} \<and> A \<le> Field r"
   using A_def dir_image_Field[of r f] SUB NE by blast
   then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
-  using WF unfolding wf_eq_minimal2 by blast
+  using WF unfolding wf_eq_minimal2 by metis
   have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
   proof(clarify)
     fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
@@ -1290,7 +1290,7 @@
      }
      moreover
      {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
-      hence ?thesis using Case4 0 unfolding bsqr_def by auto
+      hence ?thesis using Case4 0 unfolding bsqr_def by force
      }
      moreover
      {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Fun_More.thy
--- a/src/HOL/Cardinals/Fun_More.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Fun_More.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -73,7 +73,7 @@
     unfolding inj_on_def by auto
   next
     fix y assume ****: "y \<in> Y"
-    with *** obtain x where "x \<in> X \<and> f x = f y" by force
+    with *** obtain x where "x \<in> X \<and> f x = f y" by atomize_elim force
     with **** * ** assms show "y \<in> X"
     unfolding inj_on_def by auto
   qed
diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Fun_More_Base.thy
--- a/src/HOL/Cardinals/Fun_More_Base.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Fun_More_Base.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -32,7 +32,7 @@
         IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A"
 shows "bij_betw f A A'"
 using assms
-proof(unfold bij_betw_def inj_on_def, auto)
+proof(unfold bij_betw_def inj_on_def, safe)
   fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
   have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp
   with ** show "a = b" by simp
diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Order_Relation_More.thy
--- a/src/HOL/Cardinals/Order_Relation_More.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Order_Relation_More.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -94,7 +94,7 @@
 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]
-  show False by auto
+  show False by metis
 next
   fix b assume "b \<in> Field r" "(a, b) \<notin> r"
   with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Order_Relation_More_Base.thy
--- a/src/HOL/Cardinals/Order_Relation_More_Base.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Order_Relation_More_Base.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -63,7 +63,7 @@
   (*  *)
   fix a assume *: "a \<in> Field r"
   obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
-  using * 1 by blast
+  using * 1 by auto
   hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
   by (simp add: total_on_def)
   thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Wellorder_Embedding_Base.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -683,7 +683,7 @@
     have "wo_rel.ofilter r (rel.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 (auto simp add: wo_rel.ofilter_def)
+    have "False \<notin> g`(rel.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)
     ultimately
diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Wellorder_Relation.thy
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -11,16 +11,18 @@
 imports Wellorder_Relation_Base Wellfounded_More
 begin
 
+context wo_rel
+begin
 
 subsection {* Auxiliaries *}
 
-lemma (in wo_rel) PREORD: "Preorder r"
+lemma PREORD: "Preorder r"
 using WELL order_on_defs[of _ r] by auto
 
-lemma (in wo_rel) PARORD: "Partial_order r"
+lemma PARORD: "Partial_order r"
 using WELL order_on_defs[of _ r] by auto
 
-lemma (in wo_rel) cases_Total2:
+lemma cases_Total2:
 "\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<Longrightarrow> phi a b);
               ((b,a) \<in> r - Id \<Longrightarrow> phi a b); (a = b \<Longrightarrow> phi a b)\<rbrakk>
              \<Longrightarrow> phi a b"
@@ -29,7 +31,7 @@
 
 subsection {* Well-founded induction and recursion adapted to non-strict well-order relations  *}
 
-lemma (in wo_rel) worec_unique_fixpoint:
+lemma worec_unique_fixpoint:
 assumes ADM: "adm_wo H" and fp: "f = H f"
 shows "f = worec H"
 proof-
@@ -44,7 +46,7 @@
 
 subsubsection {* Properties of max2 *}
 
-lemma (in wo_rel) max2_iff:
+lemma max2_iff:
 assumes "a \<in> Field r" and "b \<in> Field r"
 shows "((max2 a b, c) \<in> r) = ((a,c) \<in> r \<and> (b,c) \<in> r)"
 proof
@@ -60,7 +62,7 @@
 
 subsubsection{* Properties of minim *}
 
-lemma (in wo_rel) minim_Under:
+lemma minim_Under:
 "\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B"
 by(auto simp add: Under_def
 minim_in
@@ -74,12 +76,12 @@
 ofilter_Un
 )
 
-lemma (in wo_rel) equals_minim_Under:
+lemma equals_minim_Under:
 "\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk>
  \<Longrightarrow> a = minim B"
 by(auto simp add: Under_def equals_minim)
 
-lemma (in wo_rel) minim_iff_In_Under:
+lemma minim_iff_In_Under:
 assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
 shows "(a = minim B) = (a \<in> B \<and> a \<in> Under B)"
 proof
@@ -92,7 +94,7 @@
   using assms equals_minim_Under by simp
 qed
 
-lemma (in wo_rel) minim_Under_under:
+lemma minim_Under_under:
 assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
 shows "Under A = under (minim A)"
 proof-
@@ -128,7 +130,7 @@
   ultimately show ?thesis by blast
 qed
 
-lemma (in wo_rel) minim_UnderS_underS:
+lemma minim_UnderS_underS:
 assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
 shows "UnderS A = underS (minim A)"
 proof-
@@ -176,7 +178,7 @@
 
 subsubsection{* Properties of supr *}
 
-lemma (in wo_rel) supr_Above:
+lemma supr_Above:
 assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}"
 shows "supr B \<in> Above B"
 proof(unfold supr_def)
@@ -186,7 +188,7 @@
   using assms by (simp add: minim_in)
 qed
 
-lemma (in wo_rel) supr_greater:
+lemma supr_greater:
 assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}" and
         IN: "b \<in> B"
 shows "(b, supr B) \<in> r"
@@ -196,7 +198,7 @@
   with IN Above_def show ?thesis by simp
 qed
 
-lemma (in wo_rel) supr_least_Above:
+lemma supr_least_Above:
 assumes SUB: "B \<le> Field r" and
         ABOVE: "a \<in> Above B"
 shows "(supr B, a) \<in> r"
@@ -208,12 +210,12 @@
   by simp
 qed
 
-lemma (in wo_rel) supr_least:
+lemma supr_least:
 "\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r)\<rbrakk>
  \<Longrightarrow> (supr B, a) \<in> r"
 by(auto simp add: supr_least_Above Above_def)
 
-lemma (in wo_rel) equals_supr_Above:
+lemma equals_supr_Above:
 assumes SUB: "B \<le> Field r" and ABV: "a \<in> Above B" and
         MINIM: "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
 shows "a = supr B"
@@ -224,7 +226,7 @@
   using assms equals_minim by simp
 qed
 
-lemma (in wo_rel) equals_supr:
+lemma equals_supr:
 assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
         ABV: "\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r" and
         MINIM: "\<And> a'. \<lbrakk> a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
@@ -239,7 +241,7 @@
   using equals_supr_Above SUB by auto
 qed
 
-lemma (in wo_rel) supr_inField:
+lemma supr_inField:
 assumes "B \<le> Field r" and  "Above B \<noteq> {}"
 shows "supr B \<in> Field r"
 proof-
@@ -247,7 +249,7 @@
   thus ?thesis using assms Above_Field by auto
 qed
 
-lemma (in wo_rel) supr_above_Above:
+lemma supr_above_Above:
 assumes SUB: "B \<le> Field r" and  ABOVE: "Above B \<noteq> {}"
 shows "Above B = above (supr B)"
 proof(unfold Above_def above_def, auto)
@@ -267,7 +269,7 @@
   using 1 TRANS trans_def[of r] by blast
 qed
 
-lemma (in wo_rel) supr_under:
+lemma supr_under:
 assumes IN: "a \<in> Field r"
 shows "a = supr (under a)"
 proof-
@@ -297,12 +299,12 @@
 
 subsubsection{* Properties of successor *}
 
-lemma (in wo_rel) suc_least:
+lemma suc_least:
 "\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk>
  \<Longrightarrow> (suc B, a) \<in> r"
 by(auto simp add: suc_least_AboveS AboveS_def)
 
-lemma (in wo_rel) equals_suc:
+lemma equals_suc:
 assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
  ABVS: "\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r" and
  MINIM: "\<And> a'. \<lbrakk>a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> a' \<noteq> b \<and> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
@@ -317,7 +319,7 @@
   using equals_suc_AboveS SUB by auto
 qed
 
-lemma (in wo_rel) suc_above_AboveS:
+lemma suc_above_AboveS:
 assumes SUB: "B \<le> Field r" and
         ABOVE: "AboveS B \<noteq> {}"
 shows "AboveS B = above (suc B)"
@@ -349,7 +351,7 @@
   using assms suc_greater[of B a] 2 by auto
 qed
 
-lemma (in wo_rel) suc_singl_pred:
+lemma suc_singl_pred:
 assumes IN: "a \<in> Field r" and ABOVE_NE: "aboveS a \<noteq> {}" and
         REL: "(a',suc {a}) \<in> r" and DIFF: "a' \<noteq> suc {a}"
 shows "a' = a \<or> (a',a) \<in> r"
@@ -372,7 +374,7 @@
   thus ?thesis by blast
 qed
 
-lemma (in wo_rel) under_underS_suc:
+lemma under_underS_suc:
 assumes IN: "a \<in> Field r" and ABV: "aboveS a \<noteq> {}"
 shows "underS (suc {a}) = under a"
 proof-
@@ -410,19 +412,19 @@
 
 subsubsection {* Properties of order filters  *}
 
-lemma (in wo_rel) ofilter_INTER:
+lemma ofilter_INTER:
 "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)"
 unfolding ofilter_def by blast
 
-lemma (in wo_rel) ofilter_Inter:
+lemma ofilter_Inter:
 "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (Inter S)"
 unfolding ofilter_def by blast
 
-lemma (in wo_rel) ofilter_Union:
+lemma ofilter_Union:
 "(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (Union S)"
 unfolding ofilter_def by blast
 
-lemma (in wo_rel) ofilter_under_Union:
+lemma ofilter_under_Union:
 "ofilter A \<Longrightarrow> A = Union {under a| a. a \<in> A}"
 using ofilter_under_UNION[of A]
 by(unfold Union_eq, auto)
@@ -430,7 +432,7 @@
 
 subsubsection{* Other properties *}
 
-lemma (in wo_rel) Trans_Under_regressive:
+lemma Trans_Under_regressive:
 assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
 shows "Under(Under A) \<le> Under A"
 proof
@@ -455,7 +457,7 @@
   show "x \<in> Under A" unfolding Under_def by auto
 qed
 
-lemma (in wo_rel) ofilter_suc_Field:
+lemma ofilter_suc_Field:
 assumes OF: "ofilter A" and NE: "A \<noteq> Field r"
 shows "ofilter (A \<union> {suc A})"
 proof-
@@ -487,7 +489,7 @@
 qed
 
 (* FIXME: needed? *)
-declare (in wo_rel)
+declare
   minim_in[simp]
   minim_inField[simp]
   minim_least[simp]
@@ -499,6 +501,8 @@
   ofilter_Int[simp]
   ofilter_Un[simp]
 
+end
+
 abbreviation "worec \<equiv> wo_rel.worec"
 abbreviation "adm_wo \<equiv> wo_rel.adm_wo"
 abbreviation "isMinim \<equiv> wo_rel.isMinim"
diff -r 0051318acc9d -r 67f05cb13e08 src/HOL/Cardinals/Wellorder_Relation_Base.thy
--- a/src/HOL/Cardinals/Wellorder_Relation_Base.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Wellorder_Relation_Base.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -234,8 +234,8 @@
 assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
 shows "\<exists>b. isMinim B b"
 proof-
-  from WF wf_eq_minimal[of "r - Id"] NE Id_def obtain b where
-  *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by force
+  from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
+  *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
   show ?thesis
   proof(simp add: isMinim_def, rule exI[of _ b], auto)
     show "b \<in> B" using * by simp