# HG changeset patch
# User wenzelm
# Date 1014756453 -3600
# Node ID e4b2c9d3bf4be3b5236e506eeb58e21dd407ba68
# Parent  bf48fd86a732277acdfe4fdbd8e70a83c954cc40
quote "includes" (now a keyword);

diff -r bf48fd86a732 -r e4b2c9d3bf4b src/ZF/AC/AC16_WO4.thy
--- a/src/ZF/AC/AC16_WO4.thy	Tue Feb 26 21:47:11 2002 +0100
+++ b/src/ZF/AC/AC16_WO4.thy	Tue Feb 26 21:47:33 2002 +0100
@@ -213,7 +213,7 @@
   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"
@@ -321,9 +321,9 @@
 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)
@@ -394,7 +394,7 @@
 
 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
 
@@ -442,7 +442,7 @@
      "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"
@@ -473,7 +473,7 @@
 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])
@@ -516,7 +516,7 @@
 
 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"
@@ -531,7 +531,7 @@
 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