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]