# HG changeset patch
# User paulson
# Date 806944904 -7200
# Node ID bc3093616ba4fc1941a85f111cabd8711dbd2308
# Parent  3f460842e91953540c3e649cf521bb653fabdab9
Ran expandshort and corrected spelling of Grabczewski

diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/AC16_WO4.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC16_WO4.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
   The proof of AC16(n, k) ==> WO4(n-k)
 *)
@@ -14,9 +14,9 @@
 goalw thy [Finite_def] "!!A. [| Finite(A); 0<m; m:nat |] ==>  \
 \	EX a f. Ord(a) & domain(f) = a &  \
 \		(UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)";
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
 by (dresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1)] 1);
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (res_inst_tac [("x","n")] exI 1);
 by (res_inst_tac [("x","lam i:n. {f`i}")] exI 1);
 by (asm_full_simp_tac AC_ss 1);
@@ -104,10 +104,10 @@
 \	==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y";
 by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
 by (resolve_tac [prem RS FalseE] 1);
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [CollectE] 1);
-by (eresolve_tac [conjE] 1);
-by (eresolve_tac [swap] 1);
+by (rtac ballI 1);
+by (etac CollectE 1);
+by (etac conjE 1);
+by (etac swap 1);
 by (fast_tac (AC_cs addSEs [succ_not_lepoll_imp_eqpoll]) 1);
 val suppose_not = result();
 
@@ -127,7 +127,7 @@
 
 goal thy "!!y. [| well_ord(y,R); ~Finite(y); n:nat  \
 \	|] ==> EX z. z<=y & n eqpoll z";
-by (eresolve_tac [nat_lepoll_imp_ex_eqpoll_n] 1);
+by (etac nat_lepoll_imp_ex_eqpoll_n 1);
 by (resolve_tac [ordertype_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll
 	RSN (2, lepoll_trans)] 1 THEN (assume_tac 2));
 by (fast_tac (AC_cs addSIs [nat_le_infinite_Ord RS le_imp_lepoll]
@@ -185,18 +185,18 @@
 \	EX! w. w:t_n & z <= w; \
 \	k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0 |]  \
 \	==> EX! c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c";
-by (eresolve_tac [ballE] 1);
+by (etac ballE 1);
 by (fast_tac (FOL_cs addSIs [CollectI, cons_cons_subset,
 		eqpoll_sym RS cons_cons_eqpoll]) 2);
-by (eresolve_tac [ex1E] 1);
+by (etac ex1E 1);
 by (res_inst_tac [("a","w")] ex1I 1);
-by (resolve_tac [conjI] 1);
-by (resolve_tac [CollectI] 1);
+by (rtac conjI 1);
+by (rtac CollectI 1);
 by (fast_tac (FOL_cs addSEs [s_uI]) 1);
 by (fast_tac AC_cs 1);
 by (fast_tac AC_cs 1);
-by (eresolve_tac [allE] 1);
-by (eresolve_tac [impE] 1);
+by (etac allE 1);
+by (etac impE 1);
 by (assume_tac 2);
 by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
 val ex1_superset_a = result();
@@ -204,14 +204,14 @@
 goal thy
 	"!!A. [| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat  \
 \	|] ==> A = cons(a, B)";
-by (resolve_tac [equalityI] 1);
+by (rtac equalityI 1);
 by (fast_tac AC_cs 2);
 by (resolve_tac [Diff_eq_0_iff RS iffD1] 1);
-by (resolve_tac [equals0I] 1);
+by (rtac equals0I 1);
 by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1);
 by (dresolve_tac [eqpoll_sym RS cons_eqpoll_succ] 1);
 by (fast_tac AC_cs 1);
-by (dresolve_tac [cons_eqpoll_succ] 1);
+by (dtac cons_eqpoll_succ 1);
 by (fast_tac AC_cs 1);
 by (fast_tac (AC_cs addSIs [nat_succI]
 	addSEs [[eqpoll_sym RS eqpoll_imp_lepoll, subset_imp_lepoll] MRS
@@ -226,7 +226,7 @@
 \	|] ==> (THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c)  \
 \	Int y = cons(b, a)";
 by (dresolve_tac [ex1_superset_a RS theI] 1 THEN REPEAT (assume_tac 1));
-by (resolve_tac [set_eq_cons] 1);
+by (rtac set_eq_cons 1);
 by (REPEAT (fast_tac AC_cs 1));
 val the_eq_cons = result();
 
@@ -261,16 +261,16 @@
 \	THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c")]
 	(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
 by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
-by (resolve_tac [CollectI] 1);
-by (resolve_tac [lam_type] 1);
+by (rtac CollectI 1);
+by (rtac lam_type 1);
 by (resolve_tac [ex1_superset_a RS theI RS conjunct1] 1
 	THEN REPEAT (assume_tac 1));
-by (resolve_tac [ballI] 1);
-by (resolve_tac [ballI] 1);
+by (rtac ballI 1);
+by (rtac ballI 1);
 by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1));
 by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1));
-by (resolve_tac [impI] 1);
-by (resolve_tac [cons_eqE] 1);
+by (rtac impI 1);
+by (rtac cons_eqE 1);
 by (fast_tac AC_cs 2);
 by (dres_inst_tac [("A","THE c. ?P(c)"), ("C","y")] eq_imp_Int_eq 1);
 by (eresolve_tac [[asm_rl, the_eq_cons, the_eq_cons] MRS msubst] 1
@@ -293,7 +293,7 @@
 by (fast_tac AC_cs 1);
 by (eres_inst_tac [("x","A - {xa}")] allE 1);
 by (eres_inst_tac [("x","B - {xa}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
 by (asm_full_simp_tac (AC_ss addsimps [add_succ]) 1);
 by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1);
 by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2));
@@ -324,7 +324,7 @@
 by (fast_tac (AC_cs addSEs [eqpoll_imp_lepoll]) 1);
 by (eres_inst_tac [("x","A - {xa}")] allE 1);
 by (eres_inst_tac [("x","B - {xa}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
 by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll,
 	eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym]
 	addss (AC_ss addsimps [add_succ])) 1);
@@ -355,7 +355,7 @@
 \	m:nat; l:nat; x Int y = 0; u : x;  \
 \	ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y  \
 \	|] ==> w Int (x - {u}) eqpoll m";
-by (eresolve_tac [CollectE] 1);
+by (etac CollectE 1);
 by (resolve_tac [w_Int_eq_w_Diff RS ssubst] 1 THEN (assume_tac 1));
 by (fast_tac (AC_cs addSDs [s_u_subset RS subsetD]) 1);
 by (fast_tac (AC_cs addEs [equals0D] addSDs [bspec]
@@ -393,24 +393,24 @@
 \	w Int (x - {u})")] 
 	(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
 by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
-by (resolve_tac [CollectI] 1);
-by (resolve_tac [lam_type] 1);
-by (resolve_tac [CollectI] 1);
+by (rtac CollectI 1);
+by (rtac lam_type 1);
+by (rtac CollectI 1);
 by (fast_tac AC_cs 1);
-by (resolve_tac [w_Int_eqpoll_m] 1 THEN REPEAT (assume_tac 1));
+by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1));
 by (simp_tac AC_ss 1);
 by (REPEAT (resolve_tac [ballI, impI] 1));
 by (eresolve_tac [w_Int_eqpoll_m RSN (2, eqpoll_m_not_empty) RS not_emptyE] 1
 	THEN REPEAT (assume_tac 1));
 by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1));
 by (dresolve_tac [cons_cons_in RSN (2, bspec)] 1 THEN REPEAT (assume_tac 1));
-by (eresolve_tac [ex1_two_eq] 1);
+by (etac ex1_two_eq 1);
 by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
 by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
 val subset_s_u_lepoll_w = result();
 
 goal thy "!!k. [| 0<k; k:nat |] ==> EX l:nat. k = succ(l)";
-by (eresolve_tac [natE] 1);
+by (etac natE 1);
 by (fast_tac (empty_cs addSEs [ltE, mem_irrefl]) 1);
 by (fast_tac (empty_cs addSIs [refl, bexI]) 1);
 val ex_eq_succ = result();
@@ -422,12 +422,12 @@
 \	t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)};  \
 \	~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat  \
 \	|] ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y";
-by (resolve_tac [suppose_not] 1);
+by (rtac suppose_not 1);
 by (eresolve_tac [ex_eq_succ RS bexE] 1 THEN (assume_tac 1));
 by (hyp_subst_tac 1);
 by (res_inst_tac [("n1","xa")] (ex_subset_eqpoll_n RS exE) 1
 	THEN REPEAT (assume_tac 1));
-by (eresolve_tac [conjE] 1);
+by (etac conjE 1);
 by (forward_tac [[y_lepoll_subset_s_u, subset_s_u_lepoll_w] MRS lepoll_trans] 1
 	THEN REPEAT (assume_tac 1));
 by (contr_tac 1);
@@ -489,14 +489,14 @@
 
 goal thy "!!y r. [| well_ord(y,r); ~Finite(y); n:nat |] ==>  \
 \	EX R. well_ord({z:Pow(y). z lepoll n}, R)";
-by (eresolve_tac [nat_induct] 1);
+by (etac nat_induct 1);
 by (fast_tac (ZF_cs addSIs [well_ord_unit]
 	addss (ZF_ss addsimps [subsets_lepoll_0_eq_unit])) 1);
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (eresolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 
 	THEN REPEAT (assume_tac 1));
 by (asm_simp_tac (ZF_ss addsimps [subsets_lepoll_succ]) 1);
-by (dresolve_tac [well_ord_radd] 1 THEN (assume_tac 1));
+by (dtac well_ord_radd 1 THEN (assume_tac 1));
 by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS 
 		(eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1);
 by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1);
@@ -533,7 +533,7 @@
 by (fast_tac (AC_cs addSEs [eqpoll_sym]) 2);
 by (res_inst_tac [("a","v")] ex1I 1);
 by (fast_tac AC_cs 1);
-by (eresolve_tac [ex1E] 1);
+by (etac ex1E 1);
 by (res_inst_tac [("x","v")] allE 1 THEN (assume_tac 1));
 by (eres_inst_tac [("x","xb")] allE 1);
 by (fast_tac AC_cs 1);
@@ -576,10 +576,10 @@
 \	~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat  \
 \	|] ==> EX w:LL(t_n, succ(k), y). u:GG(t_n, succ(k), y)`w";
 by (forward_tac [exists_in_MM] 1 THEN REPEAT (assume_tac 1));
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
 by (res_inst_tac [("x","w Int y")] bexI 1);
-by (eresolve_tac [Int_in_LL] 2);
-by (rewrite_goals_tac [GG_def]);
+by (etac Int_in_LL 2);
+by (rewtac GG_def);
 by (asm_full_simp_tac (AC_ss addsimps [Int_in_LL]) 1);
 by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1
 	THEN (assume_tac 1));
@@ -611,10 +611,10 @@
 \	==> GG(t_n, k, y) ` v <= x";
 by (asm_full_simp_tac AC_ss 1);
 by (forward_tac [the_in_MM_subset] 1 THEN REPEAT (assume_tac 1));
-by (dresolve_tac [in_LL_eq_Int] 1 THEN REPEAT (assume_tac 1));
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [DiffE] 1);
-by (eresolve_tac [swap] 1);
+by (dtac in_LL_eq_Int 1 THEN REPEAT (assume_tac 1));
+by (rtac subsetI 1);
+by (etac DiffE 1);
+by (etac swap 1);
 by (fast_tac (AC_cs addEs [ssubst]) 1);
 val GG_subset = result();
 
@@ -627,16 +627,16 @@
 \	|] ==> (UN b<ordertype(LL(t_n, succ(k), y), S).  \
 \	(GG(t_n, succ(k), y)) `  \
 \	(converse(ordermap(LL(t_n, succ(k), y), S)) ` b)) = x";
-by (resolve_tac [equalityI] 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [OUN_E] 1);
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac OUN_E 1);
 by (eresolve_tac [GG_subset RS subsetD] 1 THEN TRYALL assume_tac);
 by (eresolve_tac [ordermap_bij RS bij_converse_bij RS
 		bij_is_fun RS apply_type] 1);
-by (eresolve_tac [ltD] 1);
-by (resolve_tac [subsetI] 1);
+by (etac ltD 1);
+by (rtac subsetI 1);
 by (eresolve_tac [exists_in_LL RS bexE] 1 THEN REPEAT (assume_tac 1));
-by (resolve_tac [OUN_I] 1);
+by (rtac OUN_I 1);
 by (resolve_tac [Ord_ordertype RSN (2, ltI)] 1 THEN (assume_tac 2));
 by (eresolve_tac [ordermap_type RS apply_type] 1);
 by (eresolve_tac [ordermap_bij RS bij_is_inj RS left_inverse RS ssubst] 1
@@ -666,10 +666,10 @@
 \	==> ALL b<ordertype(LL(t_n, succ(k), y), S).  \
 \	(GG(t_n, succ(k), y)) `  \
 \	(converse(ordermap(LL(t_n, succ(k), y), S)) ` b) lepoll m";
-by (resolve_tac [oallI] 1);
+by (rtac oallI 1);
 by (asm_full_simp_tac (AC_ss addsimps [ltD,
 	ordermap_bij RS bij_converse_bij RS bij_is_fun RS apply_type]) 1);
-by (resolve_tac [eqpoll_sum_imp_Diff_lepoll] 1);
+by (rtac eqpoll_sum_imp_Diff_lepoll 1);
 by (REPEAT (fast_tac (FOL_cs addSDs [ltD]
 	addSIs [eqpoll_sum_imp_Diff_lepoll, in_LL_eqpoll_n]
 	addEs [unique_superset_in_MM RS theI RS conjunct1 RS in_MM_eqpoll_n,
@@ -683,9 +683,9 @@
 
 goalw thy [AC16_def,WO4_def]
 	"!!n k. [| AC16(k #+ m, k); 0 < k; 0 < m; k:nat; m:nat |] ==> WO4(m)";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
 by (excluded_middle_tac "Finite(A)" 1);
-by (resolve_tac [lemma1] 2 THEN REPEAT (assume_tac 2));
+by (rtac lemma1 2 THEN REPEAT (assume_tac 2));
 by (resolve_tac [lemma2 RS revcut_rl] 1);
 by (REPEAT (eresolve_tac [exE, conjE] 1));
 by (eres_inst_tac [("x","A Un y")] allE 1);
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/Hartog.ML
--- a/src/ZF/AC/Hartog.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/Hartog.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/Hartog.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
   Some proofs on the Hartogs function.
 *)
@@ -14,11 +14,11 @@
 
 goalw thy [lepoll_def] "!!X. [| Ord(a); a lepoll X |] ==>  \
 \		EX Y. Y<=X & (EX R. well_ord(Y,R) & ordertype(Y,R)=a)";
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (REPEAT (resolve_tac [exI, conjI] 1));
 by (eresolve_tac [inj_is_fun RS fun_is_rel RS image_subset] 1);
-by (resolve_tac [exI] 1);
-by (resolve_tac [conjI] 1);
+by (rtac exI 1);
+by (rtac conjI 1);
 by (eresolve_tac [well_ord_Memrel RSN (2, subset_refl RSN (2, 
 	restrict_bij RS bij_converse_bij) RS bij_is_inj RS well_ord_rvimage)] 1
 	THEN (assume_tac 1));
@@ -30,10 +30,10 @@
 
 goal thy "!!X. [| Ord(a); a lepoll X |] ==>  \
 \		EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)";
-by (dresolve_tac [Ord_lepoll_imp_ex_well_ord] 1 THEN (assume_tac 1));
+by (dtac Ord_lepoll_imp_ex_well_ord 1 THEN (assume_tac 1));
 by (step_tac ZF_cs 1);
 by (REPEAT (ares_tac [exI, conjI] 1));
-by (eresolve_tac [ordertype_Int] 2);
+by (etac ordertype_Int 2);
 by (fast_tac ZF_cs 1);
 val Ord_lepoll_imp_eq_ordertype = result();
 
@@ -43,7 +43,7 @@
 by (REPEAT (resolve_tac [allI,impI] 1));
 by (REPEAT (eresolve_tac [allE, impE] 1));
 by (assume_tac 1);
-by (dresolve_tac [Ord_lepoll_imp_eq_ordertype] 1 THEN (assume_tac 1));
+by (dtac Ord_lepoll_imp_eq_ordertype 1 THEN (assume_tac 1));
 by (fast_tac (ZF_cs addSIs [ReplaceI] addEs [sym]) 1);
 val Ords_lepoll_set_lemma = result();
 
@@ -52,22 +52,22 @@
 val Ords_lepoll_set = result();
 
 goal thy "EX a. Ord(a) & ~a lepoll X";
-by (resolve_tac [swap] 1);
+by (rtac swap 1);
 by (fast_tac ZF_cs 1);
-by (resolve_tac [Ords_lepoll_set] 1);
+by (rtac Ords_lepoll_set 1);
 by (fast_tac ZF_cs 1);
 val ex_Ord_not_lepoll = result();
 
 goalw thy [Hartog_def] "~ Hartog(A) lepoll A";
 by (resolve_tac [ex_Ord_not_lepoll RS exE] 1);
-by (resolve_tac [LeastI] 1);
+by (rtac LeastI 1);
 by (REPEAT (fast_tac ZF_cs 1));
 val HartogI = result();
 
 val HartogE = HartogI RS notE;
 
 goalw thy [Hartog_def] "Ord(Hartog(A))";
-by (resolve_tac [Ord_Least] 1);
+by (rtac Ord_Least 1);
 val Ord_Hartog = result();
 
 goalw thy [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P";
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/OrdQuant.ML
--- a/src/ZF/AC/OrdQuant.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/OrdQuant.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/OrdQuant.thy
     ID:         $Id$
-    Authors: 	Krzysztof Gr`abczewski and L C Paulson
+    Authors: 	Krzysztof Grabczewski and L C Paulson
 
 Quantifiers and union operator for ordinals. 
 *)
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/ROOT.ML
--- a/src/ZF/AC/ROOT.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/ROOT.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -3,7 +3,7 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
-Executes the proofs of the AC-equivalences, due to Krzysztof Gr`abczewski
+Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski
 *)
 
 ZF_build_completed;	(*Make examples fail if ZF did*)
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/Transrec2.ML
--- a/src/ZF/AC/Transrec2.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/Transrec2.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/Transrec2.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Transfinite recursion introduced to handle definitions based on the three
 cases of ordinals.
@@ -8,9 +8,6 @@
 
 open Transrec2;
 
-val AC_cs = OrdQuant_cs;
-val AC_ss = OrdQuant_ss;
-
 goal thy "transrec2(0,a,b) = a";
 by (rtac (transrec2_def RS def_transrec RS trans) 1);
 by (simp_tac ZF_ss 1);
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/WO1_AC.ML
--- a/src/ZF/AC/WO1_AC.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO1_AC.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/WO1_AC.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The proofs of WO1 ==> AC1 and WO1 ==> AC10(n) for n >= 1
 
@@ -42,10 +42,10 @@
 goalw thy [WO1_def] "!!A. [| WO1; ALL B:A. EX C:D(B). P(C,B) |]  \
 \		==> EX f. ALL B:A. P(f`B,B)";
 by (eres_inst_tac [("x","Union({{C:D(B). P(C,B)}. B:A})")] allE 1);
-by (eresolve_tac [exE] 1);
-by (dresolve_tac [ex_choice_fun] 1);
+by (etac exE 1);
+by (dtac ex_choice_fun 1);
 by (fast_tac (AC_cs addEs [RepFunE, sym RS equals0D]) 1);
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (res_inst_tac [("x","lam x:A. f`{C:D(x). P(C,x)}")] exI 1);
 by (asm_full_simp_tac AC_ss 1);
 by (fast_tac (AC_cs addSDs [RepFunI RSN (2, apply_type)]
@@ -53,16 +53,16 @@
 val lemma1 = result();
 
 goalw thy [WO1_def] "!!A. [| ~Finite(B); WO1 |] ==> |B| + |B| eqpoll  B";
-by (resolve_tac [eqpoll_trans] 1);
+by (rtac eqpoll_trans 1);
 by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll]) 2);
 by (resolve_tac [eqpoll_sym RS eqpoll_trans] 1);
 by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll]) 1);
 by (resolve_tac [cadd_def RS def_imp_eq RS subst] 1);
 by (resolve_tac [Card_cardinal RSN (2, Inf_Card_is_InfCard) RS 
 			InfCard_cdouble_eq RS ssubst] 1);
-by (resolve_tac [eqpoll_refl] 2);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [notE] 1);
+by (rtac eqpoll_refl 2);
+by (rtac notI 1);
+by (etac notE 1);
 by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_Finite] 1
 	THEN (assume_tac 2));
 by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll]) 1);
@@ -74,7 +74,7 @@
 val lemma2_2 = result();
 
 goal thy "!!f. [| f:inj(A,B); f`a = f`b; a:A; b:A |] ==> a=b";
-by (resolve_tac [inj_equality] 1);
+by (rtac inj_equality 1);
 by (TRYALL (fast_tac (AC_cs addSEs [inj_is_fun RS apply_Pair] addEs [subst])));
 val lemma = result();
 
@@ -91,7 +91,7 @@
 val [major, minor] = goalw thy AC_aux_defs 
 	"[| f : bij(D+D, B); 1 le n |] ==>  \
 \	sets_of_size_between({{f`Inl(i), f`Inr(i)}. i:D}, 2, succ(n))";
-by (rewrite_goals_tac [succ_def]);
+by (rewtac succ_def);
 by (fast_tac (AC_cs addSIs [cons_lepoll_cong, minor, lepoll_refl, InlI, InrI] 
 	addIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
 		le_imp_subset RS subset_imp_lepoll]
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/WO1_WO6.ML
--- a/src/ZF/AC/WO1_WO6.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO1_WO6.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/WO1-WO6.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
   Proofs needed to state that formulations WO1,...,WO6 are all equivalent.
   All but one WO6 ==> WO1 (placed in separate file WO6_WO1.ML)
@@ -46,12 +46,12 @@
 val surj_imp_eq = result();
 
 goalw thy WO_defs "!!Z. WO1 ==> WO4(1)";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
 by (eres_inst_tac [("x","A")] allE 1);
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (REPEAT (resolve_tac [exI, conjI] 1));
-by (eresolve_tac [Ord_ordertype] 1);
-by (resolve_tac [conjI] 1);
+by (etac Ord_ordertype 1);
+by (rtac conjI 1);
 by (eresolve_tac [ordermap_bij RS bij_converse_bij RS bij_is_fun RS
 		lam_sets RS domain_of_fun] 1);
 by (asm_simp_tac (AC_ss addsimps [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/WO1_WO7.ML
--- a/src/ZF/AC/WO1_WO7.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO1_WO7.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/WO1_WO7.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5)
 LEMMA is the sentence denoted by (**)
@@ -21,8 +21,8 @@
 
 goalw thy [WO1_def] "!!Z. ALL X. ~Finite(X) -->  \
 \		(EX R. well_ord(X,R) & ~well_ord(X,converse(R))) ==> WO1";
-by (resolve_tac [allI] 1);
-by (eresolve_tac [allE] 1);
+by (rtac allI 1);
+by (etac allE 1);
 by (excluded_middle_tac "Finite(A)" 1);
 by (fast_tac AC_cs 1);
 by (rewrite_goals_tac [Finite_def, eqpoll_def]);
@@ -47,11 +47,11 @@
     "!!a. [| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))";
 by (dresolve_tac [nat_le_infinite_Ord RS le_imp_subset] 1 
     THEN (assume_tac 1));
-by (resolve_tac [notI] 1);
+by (rtac notI 1);
 by (eres_inst_tac [("x","nat")] allE 1);
-by (eresolve_tac [disjE] 1);
+by (etac disjE 1);
 by (fast_tac (ZF_cs addSDs [nat_0I RSN (2,equals0D)]) 1);
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
 by (eres_inst_tac [("x","succ(x)")] allE 1);
 by (fast_tac (ZF_cs addSIs [nat_succI, converseI, MemrelI, 
                             nat_succI RSN (2, subsetD)]) 1);
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/WO1_WO8.ML
--- a/src/ZF/AC/WO1_WO8.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO1_WO8.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/WO1_WO8.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The proof of WO8 <-> WO1 (Rubin & Rubin p. 6)
 *)
@@ -18,9 +18,9 @@
 (* ********************************************************************** *)
 
 goalw thy WO_defs "!!Z. WO8 ==> WO1";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
 by (eres_inst_tac [("x","{{x}. x:A}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
 by (fast_tac (AC_cs addSEs [lam_sing_bij RS bij_is_inj RS
 			well_ord_rvimage]) 2);
 by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/WO2_AC16.ML
--- a/src/ZF/AC/WO2_AC16.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO2_AC16.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/WO2_AC16.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
   The proof of WO2 ==> AC16(k #+ m, k)
   
@@ -24,11 +24,11 @@
 \		V: F(i); f(z)<=V; W:F(j); f(z)<=W |]  \
 \		==> V = W";
 by (REPEAT (eresolve_tac [asm_rl, allE, impE] 1));
-by (dresolve_tac [subsetD] 1 THEN (assume_tac 1));
-by (REPEAT (dresolve_tac [ospec] 1 THEN (assume_tac 1)));
+by (dtac subsetD 1 THEN (assume_tac 1));
+by (REPEAT (dtac ospec 1 THEN (assume_tac 1)));
 by (eresolve_tac [disjI2 RSN (2, impE)] 1);
 by (fast_tac (FOL_cs addSIs [bexI]) 1);
-by (eresolve_tac [ex1_two_eq] 1 THEN (REPEAT (ares_tac [conjI] 1)));
+by (etac ex1_two_eq 1 THEN (REPEAT (ares_tac [conjI] 1)));
 val lemma3_1 = result();
 
 goal thy "!!Z. [| ALL y<x. ALL z<a. z<y | (EX Y: F(y). f(z)<=Y)  \
@@ -39,7 +39,7 @@
 by (res_inst_tac [("j","j")] (lt_Ord RS (lt_Ord RSN (2, Ord_linear_le))) 1
 	THEN (REPEAT (assume_tac 1)));
 by (eresolve_tac [lemma3_1 RS sym] 1 THEN (REPEAT (assume_tac 1)));
-by (eresolve_tac [lemma3_1] 1 THEN (REPEAT (assume_tac 1)));
+by (etac lemma3_1 1 THEN (REPEAT (assume_tac 1)));
 val lemma3 = result();
 
 goal thy "!!a. [| ALL y:x. y < a --> F(y) <= X &  \
@@ -60,32 +60,32 @@
 \		==> (UN x<x. F(x)) <= X &  \
 \		(ALL xa<a. xa < x | (EX x:UN x<x. F(x). fa(xa) <= x)  \
 \		--> (EX! Y. Y : (UN x<x. F(x)) & fa(xa) <= Y))";
-by (resolve_tac [conjI] 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [OUN_E] 1);
+by (rtac conjI 1);
+by (rtac subsetI 1);
+by (etac OUN_E 1);
 by (dresolve_tac [ltD RSN (2, bspec)] 1 THEN (assume_tac 1));
 by (eresolve_tac [lt_trans RSN (2, impE)] 1 THEN (REPEAT (assume_tac 1)));
 by (fast_tac AC_cs 1);
-by (dresolve_tac [lemma4] 1 THEN (assume_tac 1));
-by (resolve_tac [oallI] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [disjE] 1);
+by (dtac lemma4 1 THEN (assume_tac 1));
+by (rtac oallI 1);
+by (rtac impI 1);
+by (etac disjE 1);
 by (forward_tac [Limit_has_succ RSN (2, ospec)] 1 THEN (REPEAT (assume_tac 1)));
 by (dres_inst_tac [("A","a"),("x","xa")] ospec 1 THEN (assume_tac 1));
 by (eresolve_tac [lt_Ord RS le_refl RSN (2, disjI1 RSN (2, impE))] 1
 	THEN (assume_tac 1));
 by (REPEAT (eresolve_tac [ex1E, conjE] 1));
-by (resolve_tac [ex1I] 1);
-by (resolve_tac [conjI] 1 THEN (assume_tac 2));
+by (rtac ex1I 1);
+by (rtac conjI 1 THEN (assume_tac 2));
 by (eresolve_tac [Limit_has_succ RS OUN_I] 1 THEN (TRYALL assume_tac));
 by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
-by (eresolve_tac [lemma3] 1 THEN (TRYALL assume_tac));
-by (eresolve_tac [Limit_has_succ] 1 THEN (assume_tac 1));
-by (eresolve_tac [bexE] 1);
-by (resolve_tac [ex1I] 1);
-by (eresolve_tac [conjI] 1 THEN (assume_tac 1));
+by (etac lemma3 1 THEN (TRYALL assume_tac));
+by (etac Limit_has_succ 1 THEN (assume_tac 1));
+by (etac bexE 1);
+by (rtac ex1I 1);
+by (etac conjI 1 THEN (assume_tac 1));
 by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
-by (eresolve_tac [lemma3] 1 THEN (TRYALL assume_tac));
+by (etac lemma3 1 THEN (TRYALL assume_tac));
 val lemma5 = result();
 
 (* ********************************************************************** *)
@@ -105,8 +105,8 @@
 
 goal thy "!!A. [| A eqpoll a; Card(a); ~Finite(a); B lesspoll a;  \
 \	C lesspoll a |] ==> A - B - C eqpoll a";
-by (resolve_tac [Diff_lesspoll_eqpoll_Card] 1 THEN (REPEAT (assume_tac 1)));
-by (resolve_tac [Diff_lesspoll_eqpoll_Card] 1 THEN (REPEAT (assume_tac 1)));
+by (rtac Diff_lesspoll_eqpoll_Card 1 THEN (REPEAT (assume_tac 1)));
+by (rtac Diff_lesspoll_eqpoll_Card 1 THEN (REPEAT (assume_tac 1)));
 val dbl_Diff_eqpoll_Card = result();
 
 (* ********************************************************************** *)
@@ -115,12 +115,12 @@
 
 goalw thy [lesspoll_def]
 	"!!X. [| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a";
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
 by (dresolve_tac [nat_le_infinite_Ord RS le_imp_lepoll] 1
 	THEN (assume_tac 1));
-by (rewrite_goals_tac [Finite_def]);
+by (rewtac Finite_def);
 by (fast_tac (AC_cs addSEs [eqpoll_sym RS eqpoll_trans]) 2);
-by (resolve_tac [lepoll_trans] 1 THEN (assume_tac 2));
+by (rtac lepoll_trans 1 THEN (assume_tac 2));
 by (fast_tac (AC_cs addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_subset RS 
 	subset_imp_lepoll RSN (2, eqpoll_imp_lepoll RS lepoll_trans)]) 1);
 val Finite_lesspoll_infinite_Ord = result();
@@ -132,21 +132,21 @@
 
 goal thy "!!n. n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x))  \
 \	--> Finite(Union(X))";
-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]
 	addSIs [nat_0I RS nat_into_Finite] addIs [Union_0 RS ssubst]) 1);
 by (REPEAT (resolve_tac [allI, impI] 1));
 by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 THEN (assume_tac 1));
 by (res_inst_tac [("P","%z. Finite(z)")] (Union_eq_Un_Diff RS ssubst) 1
 	THEN (assume_tac 1));
-by (resolve_tac [Finite_Un] 1);
+by (rtac Finite_Un 1);
 by (fast_tac AC_cs 2);
 by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll]) 1);
 val Finite_Union_lemma = result();
 
 goal thy "!!X. [| ALL x:X. Finite(x); Finite(X) |] ==> Finite(Union(X))";
 by (eresolve_tac [Finite_def RS def_imp_iff RS iffD1 RS bexE] 1);
-by (dresolve_tac [Finite_Union_lemma] 1);
+by (dtac Finite_Union_lemma 1);
 by (fast_tac AC_cs 1);
 val Finite_Union = result();
 
@@ -173,10 +173,10 @@
 by (dresolve_tac [[bij_is_fun, subset_refl] MRS image_fun] 1);
 by (dresolve_tac [sym RS trans] 1 THEN (assume_tac 1));
 by (hyp_subst_tac 1);
-by (resolve_tac [lepoll_lesspoll_lesspoll] 1);
+by (rtac lepoll_lesspoll_lesspoll 1);
 by (eresolve_tac [lt_trans1 RSN (2, lt_Card_imp_lesspoll)] 1
 	THEN REPEAT (assume_tac 1));
-by (resolve_tac [UN_lepoll] 1
+by (rtac UN_lepoll 1
 	THEN (TRYALL (fast_tac (AC_cs addSEs [lt_Ord]))));
 val Union_lesspoll = result();
 
@@ -204,7 +204,7 @@
 
 goal thy "!!x. Ord(x) ==>  \
 \	recfunAC16(f, g, x, a) - (UN i<x. recfunAC16(f, g, i, a)) lepoll 1";
-by (eresolve_tac [Ord_cases] 1);
+by (etac Ord_cases 1);
 by (asm_simp_tac (AC_ss addsimps [recfunAC16_0,
 		empty_subsetI RS subset_imp_lepoll]) 1);
 by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit,
@@ -225,12 +225,12 @@
 goal thy "!!w. [| (LEAST i. w:F(i)) = (LEAST i. z:F(i));  \
 \	w:(UN i<a. F(i)); z:(UN i<a. F(i)) |]  \
 \	==> EX b<a. w:(F(b) - (UN c<b. F(c))) & z:(F(b) - (UN c<b. F(c)))";
-by (REPEAT (eresolve_tac [OUN_E] 1));
+by (REPEAT (etac OUN_E 1));
 by (dresolve_tac [lt_Ord RSN (2, in_Least_Diff)] 1 THEN (assume_tac 1));
 by (forward_tac [lt_Ord RSN (2, in_Least_Diff)] 1 THEN (assume_tac 1));
-by (resolve_tac [oexI] 1);
-by (resolve_tac [conjI] 1 THEN (assume_tac 2));
-by (eresolve_tac [subst] 1 THEN (assume_tac 1));
+by (rtac oexI 1);
+by (rtac conjI 1 THEN (assume_tac 2));
+by (etac subst 1 THEN (assume_tac 1));
 by (eresolve_tac [lt_Ord RSN (2, Least_le) RS lt_trans1] 1
 	THEN (REPEAT (assume_tac 1)));
 val Least_eq_imp_ex = result();
@@ -243,24 +243,24 @@
 \	==> (UN x<a. F(x)) lepoll a";
 by (resolve_tac [lepoll_def RS (def_imp_iff RS iffD2)] 1);
 by (res_inst_tac [("x","lam z: (UN x<a. F(x)). LEAST i. z:F(i)")] exI 1);
-by (rewrite_goals_tac [inj_def]);
-by (resolve_tac [CollectI] 1);
-by (resolve_tac [lam_type] 1);
-by (eresolve_tac [OUN_E] 1);
-by (eresolve_tac [Least_in_Ord] 1);
-by (eresolve_tac [ltD] 1);
-by (eresolve_tac [lt_Ord2] 1);
-by (resolve_tac [ballI] 1);
-by (resolve_tac [ballI] 1);
+by (rewtac inj_def);
+by (rtac CollectI 1);
+by (rtac lam_type 1);
+by (etac OUN_E 1);
+by (etac Least_in_Ord 1);
+by (etac ltD 1);
+by (etac lt_Ord2 1);
+by (rtac ballI 1);
+by (rtac ballI 1);
 by (asm_simp_tac AC_ss 1);
-by (resolve_tac [impI] 1);
-by (dresolve_tac [Least_eq_imp_ex] 1 THEN (REPEAT (assume_tac 1)));
+by (rtac impI 1);
+by (dtac Least_eq_imp_ex 1 THEN (REPEAT (assume_tac 1)));
 by (fast_tac (AC_cs addSEs [two_in_lepoll_1]) 1);
 val UN_lepoll_index = result();
 
 goal thy "!!y. Ord(y) ==> recfunAC16(f, fa, y, a) lepoll y";
-by (eresolve_tac [trans_induct] 1);
-by (eresolve_tac [Ord_cases] 1);
+by (etac trans_induct 1);
+by (etac Ord_cases 1);
 by (asm_simp_tac (AC_ss addsimps [recfunAC16_0, lepoll_refl]) 1);
 by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1);
 by (fast_tac (AC_cs addIs [conjI RS (expand_if RS iffD2)]
@@ -276,7 +276,7 @@
 \		A eqpoll a; y<a; ~Finite(a); Card(a); n:nat |]  \
 \		==> Union(recfunAC16(f,g,y,a)) lesspoll a";
 by (eresolve_tac [eqpoll_def RS def_imp_iff RS iffD1 RS exE] 1);
-by (resolve_tac [Union_lesspoll] 1 THEN (TRYALL assume_tac));
+by (rtac Union_lesspoll 1 THEN (TRYALL assume_tac));
 by (eresolve_tac [lt_Ord RS recfunAC16_lepoll_index] 3);
 by (eresolve_tac [[bij_is_inj, Card_is_Ord RS well_ord_Memrel] MRS
 	well_ord_rvimage] 2 THEN (assume_tac 2));
@@ -289,8 +289,8 @@
 \	k : nat; m : nat; y<a;  \
 \	fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}) |]  \
 \	==> A - Union(recfunAC16(f, fa, y, a)) - fa`y eqpoll a";
-by (resolve_tac [dbl_Diff_eqpoll_Card] 1 THEN (TRYALL assume_tac));
-by (resolve_tac [Union_recfunAC16_lesspoll] 1 THEN (REPEAT (assume_tac 1)));
+by (rtac dbl_Diff_eqpoll_Card 1 THEN (TRYALL assume_tac));
+by (rtac Union_recfunAC16_lesspoll 1 THEN (REPEAT (assume_tac 1)));
 by (eresolve_tac [add_type RS nat_succI] 1 THEN (assume_tac 1));
 by (resolve_tac [nat_succI RSN (2, bexI RS (Finite_def RS def_imp_iff RS
 	iffD2)) RS (Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1
@@ -309,10 +309,10 @@
 goal thy "!!x. [| x : Pow(A - B - fa`i); x eqpoll m;  \
 \	fa : bij(a, {x: Pow(A) . x eqpoll k}); i<a; k:nat; m:nat |]  \
 \	==> fa ` i Un x : {x: Pow(A) . x eqpoll k #+ m}";
-by (resolve_tac [CollectI] 1);
+by (rtac CollectI 1);
 by (fast_tac (AC_cs addSIs [PowD RS (PowD RSN (2, Un_least RS PowI))] 
 	addSEs [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)]) 1);
-by (resolve_tac [disj_Un_eqpoll_nat_sum] 1
+by (rtac disj_Un_eqpoll_nat_sum 1
 	THEN (TRYALL assume_tac));
 by (fast_tac (AC_cs addSIs [equals0I]) 1);
 by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)] 1
@@ -327,7 +327,7 @@
 \	--> Q(x,y)); succ(j)<a |]  \
 \	==> F(j)<=X & (ALL x<a. x<j | P(x,j) --> Q(x,j))";
 by (dresolve_tac [succI1 RSN (2, bspec)] 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
 by (resolve_tac [lt_Ord RS (succI1 RS ltI RS lt_Ord RS le_refl) RS lt_trans] 1
 	THEN (REPEAT (assume_tac 1)));
 val lemma6 = result();
@@ -371,20 +371,20 @@
 val Diffs_eq_imp_eq = result();
 
 goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
-by (eresolve_tac [nat_induct] 1);
+by (etac nat_induct 1);
 by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
 by (REPEAT (resolve_tac [allI, impI] 1));
-by (REPEAT (eresolve_tac [conjE] 1));
+by (REPEAT (etac conjE 1));
 by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1
 	THEN (assume_tac 1));
 by (forward_tac [subsetD RS Diff_sing_lepoll] 1
 	THEN REPEAT (assume_tac 1));
 by (forward_tac [lepoll_Diff_sing] 1);
 by (REPEAT (eresolve_tac [allE, impE] 1));
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
 by (fast_tac AC_cs 2);
 by (fast_tac (AC_cs addSEs [singletonE] addSIs [singletonI]) 1);
-by (eresolve_tac [Diffs_eq_imp_eq] 1
+by (etac Diffs_eq_imp_eq 1
 	THEN REPEAT (assume_tac 1));
 val subset_imp_eq_lemma = result();
 
@@ -394,8 +394,8 @@
 
 goal thy "!!f. [| f:bij(a, {Y:X. Y eqpoll succ(k)}); k:nat; f`b<=f`y; b<a;  \
 \	y<a |] ==> b=y";
-by (dresolve_tac [subset_imp_eq] 1);
-by (eresolve_tac [nat_succI] 3);
+by (dtac subset_imp_eq 1);
+by (etac nat_succI 3);
 by (fast_tac (AC_cs addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS
 		CollectE, eqpoll_sym RS eqpoll_imp_lepoll]) 1);
 by (fast_tac (AC_cs addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS
@@ -415,22 +415,22 @@
 \		(ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))";
 by (eresolve_tac [dbl_Diff_eqpoll RS ex_subset_eqpoll RS bexE] 1
 	THEN REPEAT (assume_tac 1));
-by (eresolve_tac [Card_is_Ord] 1);
+by (etac Card_is_Ord 1);
 by (forward_tac [Un_in_Collect] 2 THEN REPEAT (assume_tac 2));
-by (eresolve_tac [CollectE] 4);
-by (resolve_tac [bexI] 4);
-by (resolve_tac [CollectI] 5);
+by (etac CollectE 4);
+by (rtac bexI 4);
+by (rtac CollectI 5);
 by (assume_tac 5);
 by (eresolve_tac [add_succ RS subst] 5);
 by (assume_tac 1);
-by (eresolve_tac [nat_succI] 1);
+by (etac nat_succI 1);
 by (assume_tac 1);
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
 by (fast_tac AC_cs 1);
 by (REPEAT (resolve_tac [ballI, impI, oallI, notI] 1));
 by (dresolve_tac [Int_empty RSN (2, subset_Un_disjoint)] 1
 	THEN REPEAT (assume_tac 1));
-by (dresolve_tac [bij_imp_arg_eq] 1 THEN REPEAT (assume_tac 1));
+by (dtac bij_imp_arg_eq 1 THEN REPEAT (assume_tac 1));
 by (hyp_subst_tac 1);
 by (eresolve_tac [bexI RSN (2, notE)] 1 THEN TRYALL assume_tac);
 val ex_next_set = result();
@@ -450,8 +450,8 @@
 \	==> EX c<a. fa`y <= f`c &  \
 \		(ALL b<a. fa`b <= f`c -->  \
 \		(ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))";
-by (dresolve_tac [ex_next_set] 1 THEN REPEAT (assume_tac 1));
-by (eresolve_tac [bexE] 1);
+by (dtac ex_next_set 1 THEN REPEAT (assume_tac 1));
+by (etac bexE 1);
 by (resolve_tac [bij_converse_bij RS bij_is_fun RS apply_type RS ltI RSN
 	(2, oexI)] 1);
 by (resolve_tac [right_inverse_bij RS ssubst] 1
@@ -472,20 +472,20 @@
 \	==> F(j) Un {L} <= X &  \
 \	(ALL x<a. x le j | (EX xa:F(j) Un {L}. P(x, xa)) -->  \
 \		(EX! Y. Y:F(j) Un {L} & P(x, Y)))";
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
 by (fast_tac (AC_cs addSIs [singleton_subsetI]) 1);
-by (resolve_tac [oallI] 1);
-by (eresolve_tac [oallE] 1 THEN (contr_tac 2));
-by (resolve_tac [impI] 1);
-by (eresolve_tac [disjE] 1);
-by (eresolve_tac [leE] 1);
+by (rtac oallI 1);
+by (etac oallE 1 THEN (contr_tac 2));
+by (rtac impI 1);
+by (etac disjE 1);
+by (etac leE 1);
 by (eresolve_tac [disjI1 RSN (2, impE)] 1 THEN (assume_tac 1));
-by (resolve_tac [ex1E] 1 THEN (assume_tac 1));
-by (eresolve_tac [ex1_in_Un_sing] 1);
+by (rtac ex1E 1 THEN (assume_tac 1));
+by (etac ex1_in_Un_sing 1);
 by (fast_tac AC_cs 1);
 by (fast_tac AC_cs 1);
-by (eresolve_tac [bexE] 1);
-by (eresolve_tac [UnE] 1);
+by (etac bexE 1);
+by (etac UnE 1);
 by (fast_tac (AC_cs addSEs [ex1_in_Un_sing]) 1);
 by (fast_tac AC_cs 1);
 val lemma8 = result();
@@ -502,27 +502,27 @@
 \	==> recfunAC16(f, fa, b, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)} &  \
 \	(ALL x<a. x < b | (EX Y:recfunAC16(f, fa, b, a). fa ` x <= Y) -->  \
 \	(EX! Y. Y:recfunAC16(f, fa, b, a) & fa ` x <= Y))";
-by (resolve_tac [impE] 1 THEN (REPEAT (assume_tac 2)));
+by (rtac impE 1 THEN (REPEAT (assume_tac 2)));
 by (eresolve_tac [lt_Ord RS trans_induct] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [Ord_cases] 1);
+by (rtac impI 1);
+by (etac Ord_cases 1);
 (* case 0 *)
 by (asm_simp_tac (AC_ss addsimps [recfunAC16_0]) 1);
 by (fast_tac (AC_cs addSEs [ltE]) 1);
 (* case Limit *)
 by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit]) 2);
-by (eresolve_tac [lemma5] 2 THEN (REPEAT (assume_tac 2)));
+by (etac lemma5 2 THEN (REPEAT (assume_tac 2)));
 by (fast_tac (FOL_cs addSEs [recfunAC16_mono]) 2);
 (* case succ *)
 by (hyp_subst_tac 1);
 by (eresolve_tac [lemma6 RS conjE] 1 THEN (assume_tac 1));
 by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1);
 by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
-by (eresolve_tac [lemma7] 1 THEN (REPEAT (assume_tac 1)));
-by (resolve_tac [impI] 1);
+by (etac lemma7 1 THEN (REPEAT (assume_tac 1)));
+by (rtac impI 1);
 by (resolve_tac [ex_next_Ord RS oexE] 1 
 	THEN REPEAT (ares_tac [le_refl RS lt_trans] 1));
-by (eresolve_tac [lemma8] 1 THEN (assume_tac 1));
+by (etac lemma8 1 THEN (assume_tac 1));
 by (resolve_tac [bij_is_fun RS apply_type] 1 THEN (assume_tac 1));
 by (eresolve_tac [Least_le RS lt_trans2 RS ltD] 1 
 	THEN REPEAT (ares_tac [lt_Ord, succ_leI] 1));
@@ -540,23 +540,23 @@
 \	f:a->f``(a); Limit(a); (!!i j. i le j ==> F(i) <= F(j)) |]  \
 \	==> (UN j<a. F(j)) <= S &  \
 \	(ALL x:f``a. EX! Y. Y : (UN j<a. F(j)) & x <= Y)";
-by (resolve_tac [conjI] 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [OUN_E] 1);
-by (dresolve_tac [prem1] 1);
+by (rtac conjI 1);
+by (rtac subsetI 1);
+by (etac OUN_E 1);
+by (dtac prem1 1);
 by (fast_tac AC_cs 1);
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [imageE] 1);
+by (rtac ballI 1);
+by (etac imageE 1);
 by (dresolve_tac [prem3 RS Limit_is_Ord RSN (2, ltI) RS
 	(prem3 RS Limit_has_succ)] 1);
 by (forward_tac [prem1] 1);
-by (eresolve_tac [conjE] 1);
+by (etac conjE 1);
 by (dresolve_tac [leI RS succ_leE RSN (2, ospec)] 1 THEN (assume_tac 1));
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
 by (fast_tac (AC_cs addSEs [leI RS succ_leE RS lt_Ord RS le_refl]) 1);
 by (dresolve_tac [prem2 RSN (2, apply_equality)] 1);
 by (REPEAT (eresolve_tac [conjE, ex1E] 1));
-by (resolve_tac [ex1I] 1);
+by (rtac ex1I 1);
 by (fast_tac (AC_cs addSIs [OUN_I]) 1);
 by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
 by (eresolve_tac [lt_Ord RSN (2, lt_Ord RS Ord_linear_le)] 1 THEN (assume_tac 1));
@@ -565,10 +565,10 @@
 by (forward_tac [prem1] 1);
 by (forward_tac [succ_leE] 1);
 by (dresolve_tac [prem4 RS subsetD] 1 THEN (assume_tac 1));
-by (eresolve_tac [conjE] 1);
+by (etac conjE 1);
 by (dresolve_tac [lt_trans RSN (2, ospec)] 1 THEN (TRYALL assume_tac));
 by (dresolve_tac [disjI1 RSN (2, mp)] 1 THEN (assume_tac 1));
-by (eresolve_tac [ex1_two_eq] 1);
+by (etac ex1_two_eq 1);
 by (REPEAT (fast_tac FOL_cs 1));
 val lemma_simp_induct = result();
 
@@ -578,8 +578,8 @@
 
 goalw thy [AC16_def]
 	"!!n k. [| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)";
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
+by (rtac allI 1);
+by (rtac impI 1);
 by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1 THEN (REPEAT (assume_tac 1)));
 by (forw_inst_tac [("n","k #+ m")] (WO2_infinite_subsets_eqpoll_X) 1
 	THEN (REPEAT (ares_tac [add_type] 1)));
@@ -589,17 +589,17 @@
 	def_imp_iff RS iffD1)] 1 THEN (assume_tac 1));
 by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS
 	def_imp_iff RS iffD1)] 1 THEN (assume_tac 1));
-by (REPEAT (eresolve_tac [exE] 1));
+by (REPEAT (etac exE 1));
 by (res_inst_tac [("x","UN j<a. recfunAC16(fa,f,j,a)")] exI 1);
 by (res_inst_tac [("P","%z. ?Y & (ALL x:z. ?Z(x))")] 
 	(bij_is_surj RS surj_image_eq RS subst) 1
 	THEN (assume_tac 1));
-by (resolve_tac [lemma_simp_induct] 1);
+by (rtac lemma_simp_induct 1);
 by (eresolve_tac [bij_is_fun RS surj_image RS surj_is_fun] 2);
 by (eresolve_tac [eqpoll_imp_lepoll RS lepoll_infinite RS
 	infinite_Card_is_InfCard RS InfCard_is_Limit] 2 
 	THEN REPEAT (assume_tac 2));
-by (eresolve_tac [recfunAC16_mono] 2);
-by (resolve_tac [main_induct] 1 
+by (etac recfunAC16_mono 2);
+by (rtac main_induct 1 
 	THEN REPEAT (ares_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1));
 qed "WO2_AC16";
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/WO6_WO1.ML
--- a/src/ZF/AC/WO6_WO1.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO6_WO1.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/WO6_WO1.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The proof of "WO6 ==> WO1".  Simplified by L C Paulson.
 
@@ -111,7 +111,7 @@
 goal thy "!!a b. [| P(a, b);  Ord(a);  Ord(b);  \
 \		Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |]  \
 \		==> P(Least_a, LEAST b. P(Least_a, b))";
-by (eresolve_tac [ssubst] 1);
+by (etac ssubst 1);
 by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1);
 by (REPEAT (fast_tac (ZF_cs addSEs [LeastI]) 1));
 val nested_LeastI = result();
@@ -141,7 +141,7 @@
 by (asm_simp_tac (ZF_ss addsimps [ww1_def]) 1);
 by (excluded_middle_tac "f`(b--a) = 0" 1);
 by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]) 2);
-by (resolve_tac [Diff_lepoll] 1);
+by (rtac Diff_lepoll 1);
 by (fast_tac AC_cs 1);
 by (rtac vv1_subset 1);
 by (dtac (ospec RS mp) 1);
@@ -170,7 +170,7 @@
 goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0;  \
 \			y*y<=y;	(UN b<a. f`b)=y |]  \
 \		==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
-by (dresolve_tac [ex_d_uu_not_empty] 1 THEN REPEAT (assume_tac 1));
+by (dtac ex_d_uu_not_empty 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (AC_cs addSEs [LeastI, lt_Ord]) 1);
 val uu_not_empty = result();
 
@@ -194,12 +194,12 @@
 
 (*Could this be proved more directly?*)
 goal thy "!!A B. [| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
-by (eresolve_tac [natE] 1);
+by (etac natE 1);
 by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
 by (hyp_subst_tac 1);
-by (resolve_tac [equalityI] 1);
+by (rtac equalityI 1);
 by (assume_tac 2);
-by (resolve_tac [subsetI] 1);
+by (rtac subsetI 1);
 by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
 by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2, 
 		Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS 
@@ -246,7 +246,7 @@
 \	     ALL b<a. f`b lepoll succ(m); y*y<=y;  			\
 \	     (UN b<a.f`b)=y;  Ord(a);  m:nat;  s:f`b;  b<a		\
 \	  |] ==> (UN g<a++a. gg2(f,a,b,s) ` g) = y";
-bd sym 1;
+by (dtac sym 1);
 by (asm_simp_tac
     (OrdQuant_ss addsimps [UN_oadd, lt_oadd1,
 			   oadd_le_self RS le_imp_not_lt, lt_Ord,
@@ -278,8 +278,8 @@
 \	  |] ==> ww2(f,b,g,d) lepoll m";
 by (excluded_middle_tac "f`g = 0" 1);
 by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]) 2);
-by (dresolve_tac [ospec] 1 THEN (assume_tac 1));
-by (resolve_tac [Diff_lepoll] 1
+by (dtac ospec 1 THEN (assume_tac 1));
+by (rtac Diff_lepoll 1
 	THEN (TRYALL assume_tac));
 by (asm_simp_tac (OrdQuant_ss addsimps [vv2_def, expand_if, not_emptyI]) 1);
 val ww2_lepoll = result();
@@ -312,8 +312,8 @@
 (* case 2 *)
 by (REPEAT (eresolve_tac [oexE, conjE] 1));
 by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (assume_tac 1));
-by (resolve_tac [CollectI] 1);
-by (eresolve_tac [succ_natD] 1);
+by (rtac CollectI 1);
+by (etac succ_natD 1);
 by (res_inst_tac [("x","a++a")] exI 1);
 by (res_inst_tac [("x","gg2(f,a,b,x)")] exI 1);
 (*Calling fast_tac might get rid of the res_inst_tac calls, but it
@@ -392,25 +392,25 @@
 
 goal thy "!!f. [| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |]  \
 \		==> f` (LEAST i. f`i = {x}) = {x}";
-by (dresolve_tac [lemma1] 1 THEN REPEAT (assume_tac 1));
+by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (AC_cs addSEs [lt_Ord] addIs [LeastI]) 1);
 val lemma2 = result();
 
 goalw thy [NN_def] "!!y. 1 : NN(y) ==> EX a f. Ord(a) & f:inj(y, a)";
-by (eresolve_tac [CollectE] 1);
+by (etac CollectE 1);
 by (REPEAT (eresolve_tac [exE, conjE] 1));
 by (res_inst_tac [("x","a")] exI 1);
 by (res_inst_tac [("x","lam x:y. LEAST i. f`i = {x}")] exI 1);
-by (resolve_tac [conjI] 1 THEN (assume_tac 1));
+by (rtac conjI 1 THEN (assume_tac 1));
 by (res_inst_tac [("d","%i. THE x. x:f`i")] lam_injective 1);
-by (dresolve_tac [lemma1] 1 THEN REPEAT (assume_tac 1));
+by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (AC_cs addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
 by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (ZF_cs addSIs [the_equality]) 1);
 val NN_imp_ex_inj = result();
 
 goal thy "!!y. [| y*y <= y; 1 : NN(y) |] ==> EX r. well_ord(y, r)";
-by (dresolve_tac [NN_imp_ex_inj] 1);
+by (dtac NN_imp_ex_inj 1);
 by (fast_tac (ZF_cs addSEs [well_ord_Memrel RSN (2,  well_ord_rvimage)]) 1);
 val y_well_ord = result();
 
@@ -422,7 +422,7 @@
 	"[| n:nat; !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |]  \
 \	==> n~=0 --> P(n) --> P(1)";
 by (res_inst_tac [("n","n")] nat_induct 1);
-by (resolve_tac [prem1] 1);
+by (rtac prem1 1);
 by (fast_tac ZF_cs 1);
 by (excluded_middle_tac "x=0" 1);
 by (fast_tac ZF_cs 2);
@@ -434,7 +434,7 @@
 \	!!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |]  \
 \	==> P(1)";
 by (resolve_tac [rev_induct_lemma RS impE] 1);
-by (eresolve_tac [impE] 4 THEN (assume_tac 5));
+by (etac impE 4 THEN (assume_tac 5));
 by (REPEAT (ares_tac prems 1));
 val rev_induct = result();
 
@@ -443,8 +443,8 @@
 val NN_into_nat = result();
 
 goal thy "!!n. [| n:NN(y); y*y <= y; n~=0 |] ==> 1:NN(y)";
-by (resolve_tac [rev_induct] 1 THEN REPEAT (ares_tac [NN_into_nat] 1));
-by (resolve_tac [lemma_ii] 1 THEN REPEAT (assume_tac 1));
+by (rtac rev_induct 1 THEN REPEAT (ares_tac [NN_into_nat] 1));
+by (rtac lemma_ii 1 THEN REPEAT (assume_tac 1));
 val lemma3 = result();
 
 (* ********************************************************************** *)
@@ -458,12 +458,12 @@
 val NN_y_0 = result();
 
 goalw thy [WO1_def] "!!Z. WO6 ==> WO1";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
 by (excluded_middle_tac "A=0" 1);
 by (fast_tac (ZF_cs addSIs [well_ord_Memrel, nat_0I RS nat_into_Ord]) 2);
 by (res_inst_tac [("x1","A")] (lemma_iv RS revcut_rl) 1);
-by (eresolve_tac [exE] 1);
-by (dresolve_tac [WO6_imp_NN_not_empty] 1);
+by (etac exE 1);
+by (dtac WO6_imp_NN_not_empty 1);
 by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1);
 by (eres_inst_tac [("A","NN(y)")] not_emptyE 1);
 by (forward_tac [y_well_ord] 1);
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/WO_AC.ML
--- a/src/ZF/AC/WO_AC.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO_AC.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/WO_AC.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Lemmas used in the proofs like WO? ==> AC?
 *)
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/first.ML
--- a/src/ZF/AC/first.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/first.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/first.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Lemmas involving the first element of a well ordered set
 *)
@@ -15,7 +15,7 @@
 	"!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))";
 by (REPEAT (eresolve_tac [conjE,allE,disjE] 1));
 by (contr_tac 1);
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
 by (res_inst_tac [("a","x")] ex1I 1);
 by (fast_tac ZF_cs 2);
 by (rewrite_goals_tac [tot_ord_def, linear_def]);
@@ -23,7 +23,7 @@
 val well_ord_imp_ex1_first = result();
 
 goal thy "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B";
-by (dresolve_tac [well_ord_imp_ex1_first] 1 THEN REPEAT (assume_tac 1));
-by (resolve_tac [first_is_elem] 1);
-by (eresolve_tac [theI] 1);
+by (dtac well_ord_imp_ex1_first 1 THEN REPEAT (assume_tac 1));
+by (rtac first_is_elem 1);
+by (etac theI 1);
 val the_first_in = result();
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/recfunAC16.ML
--- a/src/ZF/AC/recfunAC16.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/recfunAC16.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/recfunAC16.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Properties of the recursive definition used in the proof of WO2 ==> AC16
 *)
@@ -12,7 +12,7 @@
 (* ********************************************************************** *)
 
 goalw thy [recfunAC16_def] "recfunAC16(f,fa,0,a) = 0";
-by (resolve_tac [transrec2_0] 1);
+by (rtac transrec2_0 1);
 val recfunAC16_0 = result();
 
 goalw thy [recfunAC16_def] "recfunAC16(f,fa,succ(i),a) =  \
@@ -20,12 +20,12 @@
 \       recfunAC16(f,fa,i,a) Un {f ` (LEAST j. fa ` i <= f ` j &  \
 \	(ALL b<a. (fa`b <= f`j  \
 \	--> (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})";
-by (resolve_tac [transrec2_succ] 1);
+by (rtac transrec2_succ 1);
 val recfunAC16_succ = result();
 
 goalw thy [recfunAC16_def] "!!i. Limit(i)  \
 \	==> recfunAC16(f,fa,i,a) = (UN j<i. recfunAC16(f,fa,j,a))";
-by (eresolve_tac [transrec2_Limit] 1);
+by (etac transrec2_Limit 1);
 val recfunAC16_Limit = result();
 
 (* ********************************************************************** *)
@@ -36,7 +36,7 @@
     "[| !!g r. r <= B(g,r); Ord(i) |]  \
 \	==> j<i --> transrec2(j, 0, B) <= transrec2(i, 0, B)";
 by (resolve_tac [prem2 RS trans_induct] 1);
-by (resolve_tac [Ord_cases] 1 THEN (REPEAT (assume_tac 1)));
+by (rtac Ord_cases 1 THEN (REPEAT (assume_tac 1)));
 by (fast_tac lt_cs 1);
 by (asm_simp_tac (AC_ss addsimps [transrec2_succ]) 1);
 by (fast_tac (FOL_cs addSIs [succI1, prem1]
@@ -59,7 +59,7 @@
 
 goalw thy [recfunAC16_def]
 	"!!i. i le j ==> recfunAC16(f, g, i, a) <= recfunAC16(f, g, j, a)";
-by (resolve_tac [transrec2_mono] 1);
+by (rtac transrec2_mono 1);
 by (REPEAT (fast_tac (AC_cs addIs [expand_if RS iffD2]) 1));
 val recfunAC16_mono = result();
 
diff -r 3f460842e919 -r bc3093616ba4 src/ZF/AC/rel_is_fun.ML
--- a/src/ZF/AC/rel_is_fun.ML	Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/rel_is_fun.ML	Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/rel_is_fun.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Lemmas needed to state when a finite relation is a function.
 
@@ -11,23 +11,23 @@
 (*Using AC we could trivially prove, for all u, domain(u) lepoll u*)
 goalw Cardinal.thy [lepoll_def]
      "!!m. [| m:nat; u lepoll m |] ==> domain(u) lepoll m";
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (res_inst_tac [("x",
 	"lam x:domain(u). LEAST i. EX y. <x,y> : u & f`<x,y> = i")] exI 1);
 by (res_inst_tac [("d","%y. fst(converse(f)`y)")] lam_injective 1);
 by (fast_tac (ZF_cs addIs [LeastI2, nat_into_Ord RS Ord_in_Ord,
 			inj_is_fun RS apply_type]) 1);
-by (eresolve_tac [domainE] 1);
+by (etac domainE 1);
 by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1));
-by (resolve_tac [LeastI2] 1);
+by (rtac LeastI2 1);
 by (REPEAT (fast_tac (ZF_cs addIs [fst_conv, left_inverse RS ssubst]
 			addSEs [nat_into_Ord RS Ord_in_Ord]) 1));
 val lepoll_m_imp_domain_lepoll_m = result();
 
 goal ZF.thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
-by (resolve_tac [equalityI] 1);
+by (rtac equalityI 1);
 by (fast_tac (ZF_cs addSIs [domain_mono]) 1);
-by (resolve_tac [subsetI] 1);
+by (rtac subsetI 1);
 by (excluded_middle_tac "x = a" 1);
 by (REPEAT (fast_tac (ZF_cs addSIs [domainI] addSEs [domainE]) 1));
 val domain_Diff_eq_domain = result();