# HG changeset patch
# User paulson
# Date 838377064 -7200
# Node ID 618f48bd45325c557b6accd6becf0a08d17629fa
# Parent  a525e960f2bd6044860c9d8a453da261d24b9c90
Addition of rev_notE

diff -r a525e960f2bd -r 618f48bd4532 src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Fri Jul 26 12:27:22 1996 +0200
+++ b/src/FOL/IFOL.ML	Fri Jul 26 12:31:04 1996 +0200
@@ -46,6 +46,9 @@
   [ (resolve_tac [mp RS FalseE] 1),
     (REPEAT (resolve_tac prems 1)) ]);
 
+qed_goal "rev_notE" IFOL.thy "!!P R. [| P; ~P |] ==> R"
+ (fn _ => [REPEAT (ares_tac [notE] 1)]);
+
 (*This is useful with the special implication rules for each kind of P. *)
 qed_goal "not_to_imp" IFOL.thy 
     "[| ~P;  (P-->False) ==> Q |] ==> Q"