# HG changeset patch
# User paulson
# Date 1084546395 -7200
# Node ID 9ccfd0f59e118a306554b50842d05ce90a51ca74
# Parent  001323d6d75bd115509bd23165e8f50d223c69e5
new atomize theorem

diff -r 001323d6d75b -r 9ccfd0f59e11 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"
diff -r 001323d6d75b -r 9ccfd0f59e11 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri May 14 16:52:53 2004 +0200
+++ b/src/HOL/simpdata.ML	Fri May 14 16:53:15 2004 +0200
@@ -72,7 +72,7 @@
 val simp_thms = thms "simp_thms";
 val split_if = thm "split_if";
 val split_if_asm = thm "split_if_asm";
-
+val atomize_not = thm"atomize_not";
 
 local
 val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"