# HG changeset patch
# User lcp
# Date 806924108 -7200
# Node ID f87457b1ce5e7472b7fa602a90b2e6f197ad56cf
# Parent  a4253da68be2d524de1322eb2b469fe134f937be
Ran expandshort and changed spelling of Grabczewski

diff -r a4253da68be2 -r f87457b1ce5e src/ZF/AC/AC15_WO6.ML
--- a/src/ZF/AC/AC15_WO6.ML	Fri Jul 28 11:20:22 1995 +0200
+++ b/src/ZF/AC/AC15_WO6.ML	Fri Jul 28 11:35:08 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC15_WO6.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The proof of AC1 ==> WO2
 *)
@@ -14,7 +14,7 @@
 val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==>  \
 \	(UN i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A";
 by (simp_tac (AC_ss addsimps [Ord_Least RS OUN_eq_UN]) 1);
-by (resolve_tac [equalityI] 1);
+by (rtac equalityI 1);
 by (fast_tac (AC_cs addSDs [less_Least_subset_x]) 1);
 by (fast_tac (AC_cs addSDs [prem RS bspec]
 		addSIs [f_subsets_imp_UN_HH_eq_x RS (Diff_eq_0_iff RS iffD1)]) 1);
@@ -22,22 +22,22 @@
 
 val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==>  \
 \	ALL x<LEAST x. HH(f,A,x)={A}. HH(f,A,x) lepoll m";
-by (resolve_tac [oallI] 1);
+by (rtac oallI 1);
 by (dresolve_tac [ltD RS less_Least_subset_x] 1);
 by (forward_tac [HH_subset_imp_eq] 1);
-by (eresolve_tac [ssubst] 1);
+by (etac ssubst 1);
 by (fast_tac (AC_cs addIs [prem RS ballE]
 		addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
 val lemma2 = result();
 
 goalw thy [AC15_def, WO6_def] "!!Z. AC15 ==> WO6";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
 by (fast_tac ZF_cs 1);
 by (REPEAT (eresolve_tac [bexE,conjE,exE] 1));
-by (resolve_tac [bexI] 1 THEN (assume_tac 2));
-by (resolve_tac [conjI] 1 THEN (assume_tac 1));
+by (rtac bexI 1 THEN (assume_tac 2));
+by (rtac conjI 1 THEN (assume_tac 1));
 by (res_inst_tac [("x","LEAST i. HH(f,A,i)={A}")] exI 1);
 by (res_inst_tac [("x","lam j: (LEAST i. HH(f,A,i)={A}). HH(f,A,j)")] exI 1);
 by (asm_full_simp_tac AC_ss 1);