diff -r b43333dc6e7d -r fb3f9887d0b7 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Jan 15 13:14:39 2002 +0100
+++ b/src/FOL/simpdata.ML	Tue Jan 15 15:07:41 2002 +0100
@@ -203,6 +203,7 @@
 int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
 prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
 
+prove     "not_imp" "~(P --> Q) <-> (P & ~Q)";
 prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
 
 prove     "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";