Added rev_notE by analogy with rev_mp

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