# HG changeset patch
# User paulson
# Date 1011103661 -3600
# Node ID fb3f9887d0b72e9a4fd7128399e899d8d3d93990
# Parent  b43333dc6e7d653048ce7182fea9035915734f25
new theorem

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))";