src/FOL/simpdata.ML
changeset 12765 fb3f9887d0b7
parent 12725 7ede865e1fe5
child 12825 f1f7964ed05c
     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))";