# HG changeset patch
# User paulson
# Date 835968473 -7200
# Node ID 149b2e69633e5a36aecc75323a5114d0c3fee813
# Parent  199243afac2b9b182b0bd3043a6efa777b412f29
Added rev_notE by analogy with rev_mp

diff -r 199243afac2b -r 149b2e69633e src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Fri Jun 28 15:26:39 1996 +0200
+++ b/src/HOL/HOL.ML	Fri Jun 28 15:27:53 1996 +0200
@@ -123,6 +123,9 @@
 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
 
+qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
+ (fn _ => [REPEAT (ares_tac [notE] 1)]);
+
 
 (** Implication **)
 section "-->";