src/ZF/AC/AC0_AC1.ML

--- a/src/ZF/AC/AC0_AC1.ML	Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/AC/AC0_AC1.ML	Fri Jan 03 15:01:55 1997 +0100
@@ -7,11 +7,11 @@
 *)
 
 goal thy "!!A. 0~:A ==> A <= Pow(Union(A))-{0}";
-by (fast_tac AC_cs 1);
+by (Fast_tac 1);
 val subset_Pow_Union = result();
 
 goal thy "!!f. [| f:(PROD X:A. X); D<=A |] ==> EX g. g:(PROD X:D. X)";
-by (fast_tac (AC_cs addSIs [restrict_type, apply_type]) 1);
+by (fast_tac (!claset addSIs [restrict_type, apply_type]) 1);
 val lemma1 = result();
 
 goalw thy AC_defs "!!Z. AC0 ==> AC1"; 
@@ -19,8 +19,8 @@
 qed "AC0_AC1";
 
 goalw thy AC_defs "!!Z. AC1 ==> AC0";
-by (deepen_tac ZF_cs 0 1);
+by (Deepen_tac 0 1);
 (*Large search space.  Faster proof by
-  by (fast_tac (FOL_cs addSIs [notI, singletonI] addSEs [notE, DiffE]) 1);
+  by (fast_tac (!claset addSIs [notI, singletonI] addSEs [notE, DiffE]) 1);
 *)
 qed "AC1_AC0";