src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Fri May 14 16:52:53 2004 +0200
+++ b/src/HOL/HOL.thy	Fri May 14 16:53:15 2004 +0200
@@ -274,6 +274,15 @@
   thus B by (rule mp)
 qed
 
+lemma atomize_not: "(A ==> False) == Trueprop (~A)"
+proof
+  assume r: "A ==> False"
+  show "~A" by (rule notI) (rule r)
+next
+  assume "~A" and A
+  thus False by (rule notE)
+qed
+
 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
 proof
   assume "x == y"