src/ZF/AC/AC16_WO4.thy

       and GG_def:    "GG  == \<lambda>v \<in> LL. (THE w. w \<in> MM & v \<subseteq> w) - v"
       and s_def:     "s(u) == {v \<in> t_n. u \<in> v & k \<lesssim> v Int y}"
   assumes all_ex:    "\<forall>z \<in> {z \<in> Pow(x Un y) . z \<approx> succ(k)}.
 	               \<exists>! w. w \<in> t_n & z \<subseteq> w "
     and disjoint[iff]:  "x Int y = 0"
-    and includes:  "t_n \<subseteq> {v \<in> Pow(x Un y). v \<approx> succ(k #+ m)}"
+    and "includes":  "t_n \<subseteq> {v \<in> Pow(x Un y). v \<approx> succ(k #+ m)}"
     and WO_R[iff]:      "well_ord(y,R)"
     and lnat[iff]:      "l \<in> nat"
     and mnat[iff]:      "m \<in> nat"
     and mpos[iff]:      "0<m"
     and Infinite[iff]:  "~ Finite(y)"

          \<forall>v \<in> s(u). succ(l) \<approx> v Int y |] 
       ==> w Int (x - {u}) \<approx> m"
 apply (erule CollectE)
 apply (subst w_Int_eq_w_Diff)
 apply (fast dest!: s_subset [THEN subsetD] 
-                   includes [simplified k_def, THEN subsetD])
+                   "includes" [simplified k_def, THEN subsetD])
 apply (blast dest: s_subset [THEN subsetD] 
-                   includes [simplified k_def, THEN subsetD] 
+                   "includes" [simplified k_def, THEN subsetD] 
              dest: eqpoll_sym [THEN cons_eqpoll_succ, THEN eqpoll_sym] 
                    in_s_imp_u_in
             intro!: eqpoll_sum_imp_Diff_eqpoll)
 done
 

 done
 
 
 lemma (in AC16) LL_subset: "LL \<subseteq> {z \<in> Pow(y). z \<lesssim> succ(k #+ m)}"
 apply (unfold LL_def MM_def)
-apply (insert includes)
+apply (insert "includes")
 apply (blast intro: subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
 done
 
 lemma (in AC16) well_ord_LL: "\<exists>S. well_ord(LL,S)"
 apply (rule well_ord_subsets_lepoll_n [THEN exE, of "succ(k#+m)"])

 
 lemma (in AC16) the_in_MM_subset:
      "v \<in> LL ==> (THE x. x \<in> MM & v \<subseteq> x) \<subseteq> x Un y"
 apply (drule unique_superset1)
 apply (unfold MM_def)
-apply (fast dest!: unique_superset1 includes [THEN subsetD])
+apply (fast dest!: unique_superset1 "includes" [THEN subsetD])
 done
 
 lemma (in AC16) GG_subset: "v \<in> LL ==> GG ` v \<subseteq> x"
 apply (unfold GG_def)
 apply (frule the_in_MM_subset)

 lemma (in AC16) exists_proper_in_s: "u \<in> x ==> \<exists>v \<in> s(u). succ(k) \<lesssim> v Int y"
 apply (rule ccontr)
 apply (subgoal_tac "\<forall>v \<in> s (u) . k \<approx> v Int y")
 prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll)
 apply (unfold k_def)
-apply (insert all_ex includes lnat)
+apply (insert all_ex "includes" lnat)
 apply (rule ex_subset_eqpoll_n [THEN exE], assumption)
 apply (rule noLepoll [THEN notE])
 apply (blast intro: lepoll_trans [OF y_lepoll_subset_s subset_s_lepoll_w])
 done
 

 (* Every element of the family is less than or equipollent to n-k (m)     *)
 (* ********************************************************************** *)
 
 lemma (in AC16) in_MM_eqpoll_n: "w \<in> MM ==> w \<approx> succ(k #+ m)"
 apply (unfold MM_def)
-apply (fast dest: includes [THEN subsetD])
+apply (fast dest: "includes" [THEN subsetD])
 done
 
 lemma (in AC16) in_LL_eqpoll_n: "w \<in> LL ==> succ(k) \<lesssim> w"
 by (unfold LL_def MM_def, fast)
 

       "well_ord(LL,S) ==>       
        \<forall>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) \<lesssim> m"
 apply (unfold GG_def)
 apply (rule oallI)
 apply (simp add: ltD ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN apply_type])
-apply (insert includes)
+apply (insert "includes")
 apply (rule eqpoll_sum_imp_Diff_lepoll)
 apply (blast del: subsetI
 	     dest!: ltD 
 	     intro!: eqpoll_sum_imp_Diff_lepoll in_LL_eqpoll_n
 	     intro: in_LL   unique_superset1 [THEN in_MM_eqpoll_n]