src/HOL/HOL.thy
changeset 14749 9ccfd0f59e11
parent 14690 f61ea8bfa81e
child 14854 61bdf2ae4dc5
     1.1 --- a/src/HOL/HOL.thy	Fri May 14 16:52:53 2004 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri May 14 16:53:15 2004 +0200
     1.3 @@ -274,6 +274,15 @@
     1.4    thus B by (rule mp)
     1.5  qed
     1.6  
     1.7 +lemma atomize_not: "(A ==> False) == Trueprop (~A)"
     1.8 +proof
     1.9 +  assume r: "A ==> False"
    1.10 +  show "~A" by (rule notI) (rule r)
    1.11 +next
    1.12 +  assume "~A" and A
    1.13 +  thus False by (rule notE)
    1.14 +qed
    1.15 +
    1.16  lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
    1.17  proof
    1.18    assume "x == y"