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";