src/HOL/simpdata.ML
changeset 1660 8cb42cd97579
parent 1655 5be64540f275
child 1722 bb326972ede6
--- a/src/HOL/simpdata.ML	Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/simpdata.ML	Wed Apr 17 17:59:58 1996 +0200
@@ -181,6 +181,9 @@
 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
 
+prove "not_all" "(~ (! x.P(x))) = (? x.~P(x))";
+prove "not_ex"  "(~ (? x.P(x))) = (! x.~P(x))";
+
 prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";
 prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";