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();