# HG changeset patch
# User nipkow
# Date 876825671 -7200
# Node ID 810fccb1ebe49347190090b264dd9210172319c8
# Parent  0cfd4f97dd3236ecb6ff67a8b776e4cdf5d0935e
Added neagtion rules for Ball and Bex.
ZF/AC now fails to build. Larry to fix.

diff -r 0cfd4f97dd32 -r 810fccb1ebe4 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Tue Oct 14 11:57:14 1997 +0200
+++ b/src/ZF/simpdata.ML	Tue Oct 14 12:41:11 1997 +0200
@@ -24,7 +24,8 @@
      "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
      "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
      "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
-     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"];
+     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
+     "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
 
 val ball_conj_distrib = 
     prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
@@ -37,7 +38,8 @@
      "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
      "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
      "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
-     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"];
+     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
+     "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
 
 val bex_disj_distrib = 
     prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";