Ran expandshort and changed spelling of Grabczewski

--- a/src/ZF/AC/AC0_AC1.ML	Fri Jul 28 11:02:22 1995 +0200
+++ b/src/ZF/AC/AC0_AC1.ML	Fri Jul 28 11:20:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC0_AC1.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 AC0 is equivalent to AC1
 AC0 comes from Suppes, AC1 from Rubin & Rubin

--- a/src/ZF/AC/AC10_AC15.ML	Fri Jul 28 11:02:22 1995 +0200
+++ b/src/ZF/AC/AC10_AC15.ML	Fri Jul 28 11:20:22 1995 +0200
@@ -28,16 +28,16 @@
 (* ********************************************************************** *)
 
 goalw thy [lepoll_def] "!!A. A~=0 ==> B lepoll A*B";
-by (eresolve_tac [not_emptyE] 1);
+by (etac not_emptyE 1);
 by (res_inst_tac [("x","lam z:B. <x,z>")] exI 1);
 by (fast_tac (AC_cs addSIs [snd_conv, lam_injective]) 1);
 val lepoll_Sigma = result();
 
 goal thy "!!A. 0~:A ==> ALL B:{cons(0,x*nat). x:A}. ~Finite(B)";
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [RepFunE] 1);
+by (rtac ballI 1);
+by (etac RepFunE 1);
 by (hyp_subst_tac 1);
-by (resolve_tac [notI] 1);
+by (rtac notI 1);
 by (dresolve_tac [subset_consI RS subset_imp_lepoll RS lepoll_Finite] 1);
 by (resolve_tac [lepoll_Sigma RS lepoll_Finite RS (nat_not_Finite RS notE)] 1
 	THEN (assume_tac 2));
@@ -50,7 +50,7 @@
 
 goalw thy [pairwise_disjoint_def]
 	"!!A. [| pairwise_disjoint(A); B:A; C:A; a:B; a:C |] ==> B=C";
-by (dresolve_tac [IntI] 1 THEN (assume_tac 1));
+by (dtac IntI 1 THEN (assume_tac 1));
 by (dres_inst_tac [("A","B Int C")] not_emptyI 1);
 by (fast_tac ZF_cs 1);
 val lemma2 = result();
@@ -60,29 +60,29 @@
 \		sets_of_size_between(f`B, 2, n) & Union(f`B)=B  \
 \	==> ALL B:A. EX! u. u:f`cons(0, B*nat) & u <= cons(0, B*nat) &  \
 \		0:u & 2 lepoll u & u lepoll n";
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [ballE] 1);
+by (rtac ballI 1);
+by (etac ballE 1);
 by (fast_tac ZF_cs 2);
-by (REPEAT (eresolve_tac [conjE] 1));
+by (REPEAT (etac conjE 1));
 by (dresolve_tac [consI1 RSN (2, lemma1)] 1);
-by (eresolve_tac [bexE] 1);
-by (resolve_tac [ex1I] 1);
+by (etac bexE 1);
+by (rtac ex1I 1);
 by (fast_tac ZF_cs 1);
-by (REPEAT (eresolve_tac [conjE] 1));
-by (resolve_tac [lemma2] 1 THEN (REPEAT (assume_tac 1)));
+by (REPEAT (etac conjE 1));
+by (rtac lemma2 1 THEN (REPEAT (assume_tac 1)));
 val lemma3 = result();
 
 goalw thy [lepoll_def] "!!A. [| A lepoll i; Ord(i) |] ==> {P(a). a:A} lepoll i";
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (res_inst_tac
 	[("x", "lam x:RepFun(A, P). LEAST j. EX a:A. x=P(a) & f`a=j")] exI 1);
 by (res_inst_tac [("d", "%y. P(converse(f)`y)")] lam_injective 1);
-by (eresolve_tac [RepFunE] 1);
+by (etac RepFunE 1);
 by (forward_tac [inj_is_fun RS apply_type] 1 THEN (assume_tac 1));
 by (fast_tac (AC_cs addIs [LeastI2]
 		addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1);
-by (eresolve_tac [RepFunE] 1);
-by (resolve_tac [LeastI2] 1);
+by (etac RepFunE 1);
+by (rtac LeastI2 1);
 by (fast_tac AC_cs 1);
 by (fast_tac (AC_cs addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1);
 by (fast_tac (AC_cs addEs [sym, left_inverse RS ssubst]) 1);
@@ -94,12 +94,12 @@
 \		(lam x:A. {fst(x). x:u(x)-{0}})`B <= B &  \
 \		(lam x:A. {fst(x). x:u(x)-{0}})`B lepoll n";
 by (asm_simp_tac AC_ss 1);
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
 by (fast_tac (empty_cs addSDs [RepFun_eq_0_iff RS iffD1]
 		addDs [lepoll_Diff_sing]
 		addEs [lepoll_trans RS succ_lepoll_natE, ssubst]
 		addSIs [notI, lepoll_refl, nat_0I]) 1);
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
 by (fast_tac (ZF_cs addSIs [fst_type] addSEs [consE]) 1);
 by (fast_tac (ZF_cs addSEs [equalityE,
 		Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1);
@@ -124,7 +124,7 @@
 (* ********************************************************************** *)
 
 goalw thy AC_defs "!!Z. [| n:nat; 1 le n; AC10(n) |] ==> AC11";
-by (resolve_tac [bexI] 1 THEN (assume_tac 2));
+by (rtac bexI 1 THEN (assume_tac 2));
 by (fast_tac ZF_cs 1);
 qed "AC10_AC11";
 
@@ -142,9 +142,9 @@
 
 goalw thy AC_defs "!!Z. AC12 ==> AC15";
 by (safe_tac ZF_cs);
-by (eresolve_tac [allE] 1);
-by (eresolve_tac [impE] 1);
-by (eresolve_tac [cons_times_nat_not_Finite] 1);
+by (etac allE 1);
+by (etac impE 1);
+by (etac cons_times_nat_not_Finite 1);
 by (fast_tac (ZF_cs addSIs [ex_fun_AC13_AC15]) 1);
 qed "AC12_AC15";
 
@@ -181,11 +181,11 @@
 (* ********************************************************************** *)
 
 goalw thy AC_defs "!!Z. AC1 ==> AC13(1)";
-by (resolve_tac [allI] 1);
-by (eresolve_tac [allE] 1);
-by (resolve_tac [impI] 1);
+by (rtac allI 1);
+by (etac allE 1);
+by (rtac impI 1);
 by (mp_tac 1);
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
 by (res_inst_tac [("x","lam x:A. {f`x}")] exI 1);
 by (asm_full_simp_tac (AC_ss addsimps
 		[singleton_eqpoll_1 RS eqpoll_imp_lepoll,
@@ -198,7 +198,7 @@
 (* ********************************************************************** *)
 
 goalw thy AC_defs "!!m n. [| m:nat; n:nat; m le n; AC13(m) |] ==> AC13(n)";
-by (dresolve_tac [nat_le_imp_lepoll] 1 THEN REPEAT (assume_tac 1));
+by (dtac nat_le_imp_lepoll 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (ZF_cs addSEs [lepoll_trans]) 1);
 qed "AC13_mono";
 
@@ -236,9 +236,9 @@
 
 goal thy "!!f. ALL B:A. f(B)~=0 & f(B)<=B & f(B) lepoll 1  \
 \		==> (lam x:A. THE y. f(x)={y}) : (PROD X:A. X)";
-by (resolve_tac [lam_type] 1);
-by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
-by (REPEAT (eresolve_tac [conjE] 1));
+by (rtac lam_type 1);
+by (dtac bspec 1 THEN (assume_tac 1));
+by (REPEAT (etac conjE 1));
 by (eresolve_tac [lemma_aux RS exE] 1 THEN (assume_tac 1));
 by (asm_full_simp_tac (AC_ss addsimps [the_element]) 1);
 by (fast_tac (AC_cs addEs [ssubst]) 1);

--- a/src/ZF/AC/recfunAC16.thy	Fri Jul 28 11:02:22 1995 +0200
+++ b/src/ZF/AC/recfunAC16.thy	Fri Jul 28 11:20:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/recfunAC16.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 A recursive definition used in the proof of WO2 ==> AC16
 *)