Ran expandshort and changed spelling of Grabczewski

--- a/src/ZF/AC/AC16_lemmas.ML	Fri Jul 28 11:35:08 1995 +0200
+++ b/src/ZF/AC/AC16_lemmas.ML	Fri Jul 28 11:48:55 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC16_lemmas.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Lemmas used in the proofs concerning AC16
 *)
@@ -12,16 +12,16 @@
 val cons_Diff_eq = result();
 
 goalw thy [lepoll_def] "1 lepoll X <-> (EX x. x:X)";
-by (resolve_tac [iffI] 1);
+by (rtac iffI 1);
 by (fast_tac (ZF_cs addIs [inj_is_fun RS apply_type]) 1);
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (res_inst_tac [("x","lam a:1. x")] exI 1);
 by (fast_tac (ZF_cs addSIs [lam_injective]) 1);
 val nat_1_lepoll_iff = result();
 
 goal thy "X eqpoll 1 <-> (EX x. X={x})";
-by (resolve_tac [iffI] 1);
-by (eresolve_tac [eqpollE] 1);
+by (rtac iffI 1);
+by (etac eqpollE 1);
 by (dresolve_tac [nat_1_lepoll_iff RS iffD1] 1);
 by (fast_tac (ZF_cs addSIs [lepoll_1_is_sing]) 1);
 by (fast_tac (ZF_cs addSIs [singleton_eqpoll_1]) 1);
@@ -33,21 +33,21 @@
 val cons_eqpoll_succ = result();
 
 goal thy "{Y:Pow(X). Y eqpoll 1} = {{x}. x:X}";
-by (resolve_tac [equalityI] 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [CollectE] 1);
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac CollectE 1);
 by (dresolve_tac [eqpoll_1_iff_singleton RS iffD1] 1);
 by (fast_tac (AC_cs addSIs [RepFunI]) 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [RepFunE] 1);
-by (resolve_tac [CollectI] 1);
+by (rtac subsetI 1);
+by (etac RepFunE 1);
+by (rtac CollectI 1);
 by (fast_tac AC_cs 1);
 by (fast_tac (AC_cs addSIs [singleton_eqpoll_1]) 1);
 val subsets_eqpoll_1_eq = result();
 
 goalw thy [eqpoll_def, bij_def] "X eqpoll {{x}. x:X}";
 by (res_inst_tac [("x","lam x:X. {x}")] exI 1);
-by (resolve_tac [IntI] 1);
+by (rtac IntI 1);
 by (rewrite_goals_tac [inj_def, surj_def]);
 by (asm_full_simp_tac AC_ss 1);
 by (fast_tac (AC_cs addSIs [lam_type, RepFunI] 
@@ -76,15 +76,15 @@
 by (res_inst_tac [("x","lam y:{y:Pow(x). y eqpoll succ(succ(n))}. \
 \		<LEAST i. i:y, y-{LEAST i. i:y}>")] exI 1);
 by (res_inst_tac [("d","%z. cons(fst(z),snd(z))")] lam_injective 1);
-by (resolve_tac [SigmaI] 1);
-by (eresolve_tac [CollectE] 1);
+by (rtac SigmaI 1);
+by (etac CollectE 1);
 by (asm_full_simp_tac AC_ss 3);
-by (resolve_tac [equalityI] 3);
+by (rtac equalityI 3);
 by (fast_tac AC_cs 4);
-by (resolve_tac [subsetI] 3);
-by (eresolve_tac [consE] 3);
+by (rtac subsetI 3);
+by (etac consE 3);
 by (fast_tac AC_cs 4);
-by (resolve_tac [CollectI] 2);
+by (rtac CollectI 2);
 by (fast_tac AC_cs 2);
 by (resolve_tac [PowD RS subsetD] 1 THEN (assume_tac 1));
 by (REPEAT (fast_tac (AC_cs addSIs [Diff_sing_eqpoll]
@@ -92,13 +92,13 @@
 val subsets_lepoll_lemma1 = result();
 
 val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> z <= succ(Union(z))";
-by (resolve_tac [subsetI] 1);
+by (rtac subsetI 1);
 by (res_inst_tac [("Q","ALL y:z. y<=x")] (excluded_middle RS disjE) 1);
 by (fast_tac (AC_cs addSIs [equalityI]) 2);
-by (eresolve_tac [swap] 1);
-by (resolve_tac [ballI] 1);
-by (resolve_tac [Ord_linear_le] 1);
-by (dresolve_tac [le_imp_subset] 3 THEN (assume_tac 3));
+by (etac swap 1);
+by (rtac ballI 1);
+by (rtac Ord_linear_le 1);
+by (dtac le_imp_subset 3 THEN (assume_tac 3));
 by (fast_tac (AC_cs addDs prems) 1);
 by (fast_tac (AC_cs addDs prems) 1);
 by (fast_tac (AC_cs addSEs [leE,ltE]) 1);
@@ -128,38 +128,38 @@
 
 goal thy "!!n. n:nat ==>  \
 \	ALL z. (ALL y:z. Ord(y)) & z eqpoll n & z~=0 --> Union(z) : z";
-by (eresolve_tac [nat_induct] 1);
+by (etac nat_induct 1);
 by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1);
 by (REPEAT (resolve_tac [allI, impI] 1));
-by (eresolve_tac [natE] 1);
+by (etac natE 1);
 by (fast_tac (AC_cs addSDs [eqpoll_1_iff_singleton RS iffD1]
 	addSIs [Union_singleton]) 1);
 by (hyp_subst_tac 1);
 by (REPEAT (eresolve_tac [conjE, not_emptyE] 1));
 by (eres_inst_tac [("x","z-{xb}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
 by (fast_tac (AC_cs addSEs [Diff_sing_eqpoll,
 		Diff_sing_eqpoll RS eqpoll_succ_imp_not_empty]) 1);
 by (resolve_tac [Union_eq_Un RSN (2, subst_elem)] 1 THEN (assume_tac 2));
 by (forward_tac [bspec] 1 THEN (assume_tac 1));
 by (dresolve_tac [Diff_subset RS subsetD RSN (2, bspec)] 1 THEN (assume_tac 1));
-by (dresolve_tac [Un_Ord_disj] 1 THEN (assume_tac 1));
-by (eresolve_tac [DiffE] 1);
-by (eresolve_tac [disjE] 1);
-by (eresolve_tac [subst_elem] 1 THEN (assume_tac 1));
-by (resolve_tac [subst_elem] 1 THEN (TRYALL assume_tac));
+by (dtac Un_Ord_disj 1 THEN (assume_tac 1));
+by (etac DiffE 1);
+by (etac disjE 1);
+by (etac subst_elem 1 THEN (assume_tac 1));
+by (rtac subst_elem 1 THEN (TRYALL assume_tac));
 val Union_in_lemma = result();
 
 goal thy "!!z. [| ALL x:z. Ord(x); z eqpoll n; z~=0; n:nat |]  \
 \		==> Union(z) : z";
-by (dresolve_tac [Union_in_lemma] 1);
+by (dtac Union_in_lemma 1);
 by (fast_tac FOL_cs 1);
 val Union_in = result();
 
 goal thy "!!x. [| InfCard(x); z:Pow(x); z eqpoll n; n:nat |]  \
 \		==> succ(Union(z)) : x";
 by (resolve_tac [Limit_has_succ RS ltE] 1 THEN (assume_tac 3));
-by (eresolve_tac [InfCard_is_Limit] 1);
+by (etac InfCard_is_Limit 1);
 by (excluded_middle_tac "z=0" 1);
 by (fast_tac (AC_cs addSIs [InfCard_is_Limit RS Limit_has_0]
 	addIs [Union_0 RS ssubst]) 2);
@@ -178,10 +178,10 @@
 \	cons(succ(Union(z)), z)")] exI 1);
 by (res_inst_tac [("d","%z. z-{Union(z)}")] lam_injective 1);
 by (resolve_tac [Union_cons_eq_succ_Union RS ssubst] 2);
-by (resolve_tac [cons_Diff_eq] 2);
+by (rtac cons_Diff_eq 2);
 by (fast_tac (AC_cs addSDs [InfCard_is_Card RS Card_is_Ord]
 	addEs [Ord_in_Ord] addSIs [succ_Union_not_mem]) 2);
-by (resolve_tac [CollectI] 1);
+by (rtac CollectI 1);
 by (fast_tac (AC_cs addSEs [cons_eqpoll_succ] 
                     addSIs [succ_Union_not_mem] 
                     addSDs [InfCard_is_Card RS Card_is_Ord] 
@@ -191,9 +191,9 @@
 
 goal thy "!!X. [| InfCard(X); n:nat |]  \
 \	==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
-by (eresolve_tac [nat_induct] 1);
-by (resolve_tac [subsets_eqpoll_1_eqpoll] 1);
-by (resolve_tac [eqpollI] 1);
+by (etac nat_induct 1);
+by (rtac subsets_eqpoll_1_eqpoll 1);
+by (rtac eqpollI 1);
 by (resolve_tac [subsets_lepoll_lemma1 RS lepoll_trans] 1 
 	THEN (REPEAT (assume_tac 1)));
 by (resolve_tac [InfCard_is_Card RS Card_is_Ord RS well_ord_Memrel RS
@@ -219,7 +219,7 @@
 
 goalw thy [eqpoll_def] "!!A B. A eqpoll B  \
 \	==> {Y:Pow(A). Y eqpoll n} eqpoll {Y:Pow(B). Y eqpoll n}";
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (res_inst_tac [("x","lam X:{Y:Pow(A). EX f. f : bij(Y, n)}. f``X")] exI 1);
 by (res_inst_tac [("d","%Z. converse(f)``Z")] lam_bijective 1);
 by (fast_tac (AC_cs
@@ -250,14 +250,14 @@
 
 goal thy "!!X n. [| WO2; n:nat; ~Finite(X) |]  \
 \	==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
-by (dresolve_tac [WO2_imp_ex_Card] 1);
+by (dtac WO2_imp_ex_Card 1);
 by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
 by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1));
-by (dresolve_tac [infinite_Card_is_InfCard] 1 THEN (assume_tac 1));
+by (dtac infinite_Card_is_InfCard 1 THEN (assume_tac 1));
 by (resolve_tac [eqpoll_trans RS eqpoll_trans] 1);
-by (eresolve_tac [subsets_eqpoll] 1);
-by (eresolve_tac [subsets_eqpoll_X] 1 THEN (assume_tac 1));
-by (eresolve_tac [eqpoll_sym] 1);
+by (etac subsets_eqpoll 1);
+by (etac subsets_eqpoll_X 1 THEN (assume_tac 1));
+by (etac eqpoll_sym 1);
 val WO2_infinite_subsets_eqpoll_X = result();
 
 goal thy "!!X. well_ord(X,R) ==> EX a. Card(a) & X eqpoll a";
@@ -267,13 +267,13 @@
 
 goal thy "!!X n. [| well_ord(X,R); n:nat; ~Finite(X) |]  \
 \		==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
-by (dresolve_tac [well_ord_imp_ex_Card] 1);
+by (dtac well_ord_imp_ex_Card 1);
 by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
 by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1));
-by (dresolve_tac [infinite_Card_is_InfCard] 1 THEN (assume_tac 1));
+by (dtac infinite_Card_is_InfCard 1 THEN (assume_tac 1));
 by (resolve_tac [eqpoll_trans RS eqpoll_trans] 1);
-by (eresolve_tac [subsets_eqpoll] 1);
-by (eresolve_tac [subsets_eqpoll_X] 1 THEN (assume_tac 1));
-by (eresolve_tac [eqpoll_sym] 1);
+by (etac subsets_eqpoll 1);
+by (etac subsets_eqpoll_X 1 THEN (assume_tac 1));
+by (etac eqpoll_sym 1);
 val well_ord_infinite_subsets_eqpoll_X = result();
 

--- a/src/ZF/AC/AC17_AC1.ML	Fri Jul 28 11:35:08 1995 +0200
+++ b/src/ZF/AC/AC17_AC1.ML	Fri Jul 28 11:48:55 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC17_AC1.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The proof of AC1 ==> AC17
 *)
@@ -15,7 +15,7 @@
 \	HH(lam X:Pow(x)-{0}. {f`X}, x, j)) = 0;  \
 \	f : Pow(x)-{0} -> x |]  \
 \	==> EX r. well_ord(x,r)";
-by (resolve_tac [exI] 1);
+by (rtac exI 1);
 by (eresolve_tac [[bij_Least_HH_x RS bij_converse_bij RS bij_is_inj,
 		Ord_Least RS well_ord_Memrel] MRS well_ord_rvimage] 1);
 by (assume_tac 1);
@@ -27,13 +27,13 @@
 
 goalw thy AC_defs "!!Z. ~AC1 ==>  \
 \		EX A. ALL f:Pow(A)-{0} -> A. EX u:Pow(A)-{0}. f`u ~: u";
-by (eresolve_tac [swap] 1);
-by (resolve_tac [allI] 1);
-by (eresolve_tac [swap] 1);
+by (etac swap 1);
+by (rtac allI 1);
+by (etac swap 1);
 by (res_inst_tac [("x","Union(A)")] exI 1);
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [swap] 1);
-by (resolve_tac [impI] 1);
+by (rtac ballI 1);
+by (etac swap 1);
+by (rtac impI 1);
 by (fast_tac (AC_cs addSIs [restrict_type]) 1);
 val not_AC1_imp_ex = result();
 
@@ -42,13 +42,13 @@
 \	x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}).  \
 \	HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0 |] \
 \	==> P";
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
 by (eresolve_tac [UN_eq_imp_well_ord RS exE] 1 THEN (assume_tac 1));
 by (eresolve_tac [ex_choice_fun_Pow RS exE] 1);
-by (eresolve_tac [ballE] 1);
+by (etac ballE 1);
 by (fast_tac (FOL_cs addEs [bexE, notE, apply_type]) 1);
-by (eresolve_tac [notE] 1);
-by (resolve_tac [Pi_type] 1 THEN (assume_tac 1));
+by (etac notE 1);
+by (rtac Pi_type 1 THEN (assume_tac 1));
 by (resolve_tac [apply_type RSN (2, subsetD)] 1 THEN TRYALL assume_tac);
 by (fast_tac AC_cs 1);
 val lemma1 = result();
@@ -72,22 +72,22 @@
 val lemma4 = result();
 
 goalw thy [AC17_def] "!!Z. AC17 ==> AC1";
-by (resolve_tac [classical] 1);
+by (rtac classical 1);
 by (eresolve_tac [not_AC1_imp_ex RS exE] 1);
 by (excluded_middle_tac
 	"EX f: Pow(x)-{0}->x. \
 \	x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}).  \
 \	HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0" 1);
-by (eresolve_tac [lemma1] 2 THEN (assume_tac 2));
-by (dresolve_tac [lemma2] 1);
-by (eresolve_tac [allE] 1);
-by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
-by (dresolve_tac [lemma4] 1);
-by (eresolve_tac [bexE] 1);
-by (dresolve_tac [apply_type] 1 THEN (assume_tac 1));
+by (etac lemma1 2 THEN (assume_tac 2));
+by (dtac lemma2 1);
+by (etac allE 1);
+by (dtac bspec 1 THEN (assume_tac 1));
+by (dtac lemma4 1);
+by (etac bexE 1);
+by (dtac apply_type 1 THEN (assume_tac 1));
 by (dresolve_tac [beta RS sym RSN (2, subst_elem)] 1);
 by (assume_tac 1);
-by (dresolve_tac [lemma3] 1 THEN (assume_tac 1));
+by (dtac lemma3 1 THEN (assume_tac 1));
 by (fast_tac (AC_cs addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem),
 		f_subset_imp_HH_subset] addSEs [mem_irrefl]) 1);
 qed "AC17_AC1";

--- a/src/ZF/AC/AC18_AC19.ML	Fri Jul 28 11:35:08 1995 +0200
+++ b/src/ZF/AC/AC18_AC19.ML	Fri Jul 28 11:48:55 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC18_AC19.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The proof of AC1 ==> AC18 ==> AC19 ==> AC1
 *)
@@ -13,22 +13,22 @@
 
 goal thy "!!f. [| f: (PROD b:{P(a). a:A}. b); ALL a:A. P(a)<=Q(a) |]  \
 \		==> (lam a:A. f`P(a)):(PROD a:A. Q(a))";
-by (resolve_tac [lam_type] 1);
-by (dresolve_tac [apply_type] 1);
-by (resolve_tac [RepFunI] 1 THEN (assume_tac 1));
-by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
-by (eresolve_tac [subsetD] 1 THEN (assume_tac 1));
+by (rtac lam_type 1);
+by (dtac apply_type 1);
+by (rtac RepFunI 1 THEN (assume_tac 1));
+by (dtac bspec 1 THEN (assume_tac 1));
+by (etac subsetD 1 THEN (assume_tac 1));
 val PROD_subsets = result();
 
 goal thy "!!X. [| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==>  \
 \  (INT a:A. UN b:B(a). X(a, b)) <= (UN f:PROD a:A. B(a). INT a:A. X(a, f`a))";
-by (resolve_tac [subsetI] 1);
+by (rtac subsetI 1);
 by (eres_inst_tac [("x","{{b:B(a). x:X(a,b)}. a:A}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
 by (fast_tac (AC_cs addSEs [RepFunE] addSDs [INT_E]
 		addEs [UN_E, sym RS equals0D]) 1);
-by (eresolve_tac [exE] 1);
-by (resolve_tac [UN_I] 1);
+by (etac exE 1);
+by (rtac UN_I 1);
 by (fast_tac (AC_cs addSEs [PROD_subsets]) 1);
 by (simp_tac AC_ss 1);
 by (fast_tac (FOL_cs addSEs [not_emptyE] addDs [RepFunI RSN (2, apply_type)]
@@ -46,7 +46,7 @@
 (* ********************************************************************** *)
 
 val [prem] = goalw thy [AC18_def, AC19_def] "AC18 ==> AC19";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
 by (res_inst_tac [("B1","%x.x")] (forall_elim_vars 0 prem RS revcut_rl) 1);
 by (fast_tac AC_cs 1);
 qed "AC18_AC19";
@@ -64,10 +64,10 @@
 
 goal thy "!!c. [|c : a; x = c Un {0}; x ~: a |] ==> x - {0} : a";
 by (hyp_subst_tac 1);
-by (resolve_tac [subst_elem] 1 THEN (assume_tac 1));
-by (resolve_tac [equalityI] 1);
+by (rtac subst_elem 1 THEN (assume_tac 1));
+by (rtac equalityI 1);
 by (fast_tac AC_cs 1);
-by (resolve_tac [subsetI] 1);
+by (rtac subsetI 1);
 by (excluded_middle_tac "x=0" 1);
 by (fast_tac AC_cs 1);
 by (fast_tac (AC_cs addEs [notE, subst_elem] addSIs [equalityI])  1);
@@ -81,12 +81,12 @@
 val lemma1_2 = result();
 
 goal thy  "!!A. EX f. f: (PROD B:{u_(a). a:A}. B) ==> EX f. f: (PROD B:A. B)";
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (res_inst_tac
 	[("x","lam a:A. if(f`(u_(a)) : a, f`(u_(a)), f`(u_(a))-{0})")] exI 1);
-by (resolve_tac [lam_type] 1);
+by (rtac lam_type 1);
 by (split_tac [expand_if] 1);
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
 by (fast_tac AC_cs 1);
 by (fast_tac (AC_cs addSEs [lemma1_2]) 1);
 val lemma1 = result();
@@ -96,7 +96,7 @@
 val lemma2_1 = result();
 
 goal thy "!!A C. [| A~=0; 0~:A |] ==> (INT x:{u_(a). a:A}. UN b:x. b) ~= 0";
-by (eresolve_tac [not_emptyE] 1);
+by (etac not_emptyE 1);
 by (res_inst_tac [("a","0")] not_emptyI 1);
 by (fast_tac (AC_cs addSIs [INT_I, RepFunI, lemma2_1] addSEs [RepFunE]) 1);
 val lemma2 = result();
@@ -110,10 +110,10 @@
 by (excluded_middle_tac "A=0" 1);
 by (fast_tac (AC_cs addSIs [empty_fun]) 2);
 by (eres_inst_tac [("x","{u_(a). a:A}")] allE 1);
-by (eresolve_tac [impE] 1);
-by (eresolve_tac [RepRep_conj] 1 THEN (assume_tac 1));
-by (resolve_tac [lemma1] 1);
-by (dresolve_tac [lemma2] 1 THEN (assume_tac 1));
+by (etac impE 1);
+by (etac RepRep_conj 1 THEN (assume_tac 1));
+by (rtac lemma1 1);
+by (dtac lemma2 1 THEN (assume_tac 1));
 by (dres_inst_tac [("P","%x. x~=0")] subst 1 THEN (assume_tac 1));
 by (fast_tac (AC_cs addSEs [lemma3 RS not_emptyE]) 1);
 qed "AC19_AC1";

--- a/src/ZF/AC/AC1_AC17.ML	Fri Jul 28 11:35:08 1995 +0200
+++ b/src/ZF/AC/AC1_AC17.ML	Fri Jul 28 11:48:55 1995 +0200
@@ -1,25 +1,25 @@
 (*  Title: 	ZF/AC/AC1_AC17.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The proof of AC1 ==> AC17
 *)
 
 goal thy "!!f. f : (PROD X:Pow(A) - {0}. X) ==> f : (Pow(A) - {0} -> A)";
-by (resolve_tac [Pi_type] 1 THEN (assume_tac 1));
-by (dresolve_tac [apply_type] 1 THEN (assume_tac 1));
+by (rtac Pi_type 1 THEN (assume_tac 1));
+by (dtac apply_type 1 THEN (assume_tac 1));
 by (fast_tac AC_cs 1);
 val lemma1 = result();
 
 goalw thy AC_defs "!!Z. AC1 ==> AC17";
-by (resolve_tac [allI] 1);
-by (resolve_tac [ballI] 1);
+by (rtac allI 1);
+by (rtac ballI 1);
 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
 by (fast_tac AC_cs 1);
-by (eresolve_tac [exE] 1);
-by (resolve_tac [bexI] 1);
-by (eresolve_tac [lemma1] 2);
-by (resolve_tac [apply_type] 1 THEN (assume_tac 1));
+by (etac exE 1);
+by (rtac bexI 1);
+by (etac lemma1 2);
+by (rtac apply_type 1 THEN (assume_tac 1));
 by (fast_tac (AC_cs addSDs [lemma1] addSEs [apply_type]) 1);
 qed "AC1_AC17";

--- a/src/ZF/AC/AC1_WO2.ML	Fri Jul 28 11:35:08 1995 +0200
+++ b/src/ZF/AC/AC1_WO2.ML	Fri Jul 28 11:48:55 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC1_WO2.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The proof of AC1 ==> WO2
 *)
@@ -10,14 +10,14 @@
 val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==>  \
 \	?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})";
 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);
-by (resolve_tac [f_subsets_imp_UN_HH_eq_x] 1);
+by (rtac f_subsets_imp_UN_HH_eq_x 1);
 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));
 by (fast_tac (AC_cs addSDs [equals0D, prem RS apply_type]) 1);
 by (fast_tac (AC_cs addSIs [prem RS Pi_weaken_type]) 1);
 val lemma1 = uresult();
 
 goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
 by (fast_tac (AC_cs addSDs [lemma1] addSIs [Ord_Least]) 1);
 qed "AC1_WO2";

--- a/src/ZF/AC/AC2_AC6.ML	Fri Jul 28 11:35:08 1995 +0200
+++ b/src/ZF/AC/AC2_AC6.ML	Fri Jul 28 11:48:55 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC2_AC6.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent
 to AC0 and AC1:
@@ -25,11 +25,11 @@
 val lemma2 = result();
 
 goalw thy AC_defs "!!Z. AC1 ==> AC2"; 
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
+by (rtac allI 1);
+by (rtac impI 1);
 by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1));
 by (REPEAT (resolve_tac [exI,ballI,equalityI] 1));
-by (resolve_tac [lemma1] 2 THEN (REPEAT (assume_tac 2)));
+by (rtac lemma1 2 THEN (REPEAT (assume_tac 2)));
 by (fast_tac (AC_cs addSEs [RepFunE, lemma2] addEs [apply_type]) 1);
 qed "AC1_AC2";
 
@@ -45,7 +45,7 @@
 
 goal thy "!!A. [| X*{X} Int C = {y}; X:A |]  \
 \		==> (THE y. X*{X} Int C = {y}): X*A";
-by (resolve_tac [subst_elem] 1);
+by (rtac subst_elem 1);
 by (fast_tac (ZF_cs addSIs [the_equality]
 		addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2);
 by (fast_tac (AC_cs addSEs [equalityE, make_elim singleton_subsetD]) 1);
@@ -104,7 +104,7 @@
 goalw thy AC_defs "!!Z. AC4 ==> AC3";
 by (REPEAT (resolve_tac [allI,ballI] 1));
 by (REPEAT (eresolve_tac [allE,impE] 1));
-by (eresolve_tac [lemma1] 1);
+by (etac lemma1 1);
 by (asm_full_simp_tac (AC_ss addsimps [lemma2, lemma3]
 			addcongs [Pi_cong]) 1);
 qed "AC4_AC3";
@@ -134,14 +134,14 @@
 by (REPEAT (resolve_tac [allI,ballI] 1));
 by (REPEAT (eresolve_tac [allE,impE] 1));
 by (eresolve_tac [fun_is_rel RS converse_type] 1);
-by (eresolve_tac [exE] 1);
-by (resolve_tac [bexI] 1);
-by (resolve_tac [Pi_type] 2 THEN (assume_tac 2));
+by (etac exE 1);
+by (rtac bexI 1);
+by (rtac Pi_type 2 THEN (assume_tac 2));
 by (fast_tac (ZF_cs addSDs [apply_type]
 	addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2);
-by (resolve_tac [ballI] 1);
-by (resolve_tac [apply_equality] 1 THEN (assume_tac 2));
-by (eresolve_tac [domainE] 1);
+by (rtac ballI 1);
+by (rtac apply_equality 1 THEN (assume_tac 2));
+by (etac domainE 1);
 by (forward_tac [range_type] 1 THEN (assume_tac 1));
 by (fast_tac (ZF_cs addSEs [singletonE, converseD] addDs [apply_equality]) 1);
 qed "AC4_AC5";
@@ -156,28 +156,28 @@
 val lemma1 = result();
 
 goalw thy [range_def] "!!A. R <= A*B ==> range(lam x:R. fst(x)) = domain(R)";
-by (resolve_tac [equalityI] 1);
+by (rtac equalityI 1);
 by (fast_tac (AC_cs addSEs [lamE, Pair_inject]
 		addEs [subst_elem]
 		addSDs [converseD, Pair_fst_snd_eq]) 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [domainE] 1);
-by (resolve_tac [domainI] 1);
+by (rtac subsetI 1);
+by (etac domainE 1);
+by (rtac domainI 1);
 by (fast_tac (AC_cs addSEs [lamI RS subst_elem] addIs [fst_conv RS ssubst]) 1);
 val lemma2 = result();
 
 goal thy "!!A. [| EX f: A->C. P(f,domain(f)); A=B |] ==>  EX f: B->C. P(f,B)";
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
 by (forward_tac [domain_of_fun] 1);
 by (fast_tac ZF_cs 1);
 val lemma3 = result();
 
 goal thy "!!g. [| R <= A*B; g: C->R; ALL x:C. (lam z:R. fst(z))` (g`x) = x |] \
 \		==> (lam x:C. snd(g`x)): (PROD x:C. R``{x})";
-by (resolve_tac [lam_type] 1);
-by (dresolve_tac [apply_type] 1 THEN (assume_tac 1));
-by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
-by (resolve_tac [imageI] 1);
+by (rtac lam_type 1);
+by (dtac apply_type 1 THEN (assume_tac 1));
+by (dtac bspec 1 THEN (assume_tac 1));
+by (rtac imageI 1);
 by (resolve_tac [subsetD RS Pair_fst_snd_eq RSN (2, subst_elem)] 1
 	THEN (REPEAT (assume_tac 1)));
 by (asm_full_simp_tac AC_ss 1);