# HG changeset patch
# User chaieb
# Date 1182080362 -7200
# Node ID 9e1edc15ef52e2353ddecdf1a9bdb54b3e2ccf7a
# Parent  6472c689664f92492bfa843bc40431799f91c7fe
added Theorem all_not_ex

diff -r 6472c689664f -r 9e1edc15ef52 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Jun 17 08:56:13 2007 +0200
+++ b/src/HOL/HOL.thy	Sun Jun 17 13:39:22 2007 +0200
@@ -1061,6 +1061,7 @@
 lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
 lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover
 lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
+lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" by blast
 
 lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
 lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover