src/ZF/simpdata.ML
changeset 3859 810fccb1ebe4
parent 3840 e0baea4d485a
child 4091 771b1f6422a8
     1.1 --- a/src/ZF/simpdata.ML	Tue Oct 14 11:57:14 1997 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Tue Oct 14 12:41:11 1997 +0200
     1.3 @@ -24,7 +24,8 @@
     1.4       "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
     1.5       "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
     1.6       "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
     1.7 -     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"];
     1.8 +     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
     1.9 +     "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
    1.10  
    1.11  val ball_conj_distrib = 
    1.12      prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
    1.13 @@ -37,7 +38,8 @@
    1.14       "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
    1.15       "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
    1.16       "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
    1.17 -     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"];
    1.18 +     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
    1.19 +     "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
    1.20  
    1.21  val bex_disj_distrib = 
    1.22      prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";