src/HOL/HOL.ML
changeset 1840 149b2e69633e
parent 1725 8b7414384396
child 1918 d898eb4beb96
     1.1 --- a/src/HOL/HOL.ML	Fri Jun 28 15:26:39 1996 +0200
     1.2 +++ b/src/HOL/HOL.ML	Fri Jun 28 15:27:53 1996 +0200
     1.3 @@ -123,6 +123,9 @@
     1.4  qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
     1.5   (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
     1.6  
     1.7 +qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
     1.8 + (fn _ => [REPEAT (ares_tac [notE] 1)]);
     1.9 +
    1.10  
    1.11  (** Implication **)
    1.12  section "-->";