new theorem
authorpaulson
Tue Jan 15 15:07:41 2002 +0100 (2002-01-15 ago)
changeset 12765fb3f9887d0b7
parent 12764 b43333dc6e7d
child 12766 7d67b065925e
new theorem
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Tue Jan 15 13:14:39 2002 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Tue Jan 15 15:07:41 2002 +0100
     1.3 @@ -203,6 +203,7 @@
     1.4  int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
     1.5  prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
     1.6  
     1.7 +prove     "not_imp" "~(P --> Q) <-> (P & ~Q)";
     1.8  prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
     1.9  
    1.10  prove     "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";