# HG changeset patch
# User lcp
# Date 799061072 -7200
# Node ID d60f203eeddf712cf1b92595b6c4e3a21cff69a7
# Parent  b3f190995bc9a14384d35cee5b1af0b5e7ea6b2a
Modified proofs for new claset primitives.  The problem is that they enforce
the "most recent added rule has priority" policy more strictly now.

diff -r b3f190995bc9 -r d60f203eeddf src/ZF/AC.ML
--- a/src/ZF/AC.ML	Fri Apr 28 10:57:40 1995 +0200
+++ b/src/ZF/AC.ML	Fri Apr 28 11:24:32 1995 +0200
@@ -14,7 +14,7 @@
 by (excluded_middle_tac "A=0" 1);
 by (asm_simp_tac (ZF_ss addsimps [Pi_empty1]) 2 THEN fast_tac ZF_cs 2);
 (*The non-trivial case*)
-by (fast_tac (eq_cs addSIs [AC, nonempty]) 1);
+by (fast_tac (eq_cs addIs [AC, nonempty]) 1);
 qed "AC_Pi";
 
 (*Using dtac, this has the advantage of DELETING the universal quantifier*)
@@ -56,3 +56,8 @@
 by (ALLGOALS (fast_tac ZF_cs));
 qed "AC_func_Pow";
 
+goal AC.thy "!!A. 0 ~: A ==> EX f. f: (PROD x:A. x)";
+by (rtac AC_Pi 1);
+by (REPEAT (ares_tac [non_empty_family] 1));
+qed "AC_Pi0";
+