--- a/src/ZF/AC/AC0_AC1.ML Mon Jun 22 15:53:24 1998 +0200
+++ b/src/ZF/AC/AC0_AC1.ML Mon Jun 22 17:12:27 1998 +0200
@@ -6,19 +6,19 @@
AC0 comes from Suppes, AC1 from Rubin & Rubin
*)
-goal thy "!!A. 0~:A ==> A <= Pow(Union(A))-{0}";
+Goal "!!A. 0~:A ==> A <= Pow(Union(A))-{0}";
by (Fast_tac 1);
qed "subset_Pow_Union";
-goal thy "!!f. [| f:(PROD X:A. X); D<=A |] ==> EX g. g:(PROD X:D. X)";
+Goal "!!f. [| f:(PROD X:A. X); D<=A |] ==> EX g. g:(PROD X:D. X)";
by (fast_tac (claset() addSIs [restrict_type, apply_type]) 1);
val lemma1 = result();
-goalw thy AC_defs "!!Z. AC0 ==> AC1";
+Goalw AC_defs "!!Z. AC0 ==> AC1";
by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1);
qed "AC0_AC1";
-goalw thy AC_defs "!!Z. AC1 ==> AC0";
+Goalw AC_defs "!!Z. AC1 ==> AC0";
by (Deepen_tac 0 1);
(*Large search space. Faster proof by
by (fast_tac (claset() addSIs [notI, singletonI] addSEs [notE, DiffE]) 1);