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