# HG changeset patch
# User wenzelm
# Date 924798225 -7200
# Node ID e02c5290885d7450d5a833ac19427a8c3bd04358
# Parent  271969bb7f95ae6cbf93deaf005c3f2ec2bbf72a
single method: include not_elim, imp_elim;

diff -r 271969bb7f95 -r e02c5290885d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Apr 22 18:20:37 1999 +0200
+++ b/src/Provers/classical.ML	Thu Apr 22 18:23:45 1999 +0200
@@ -954,7 +954,7 @@
   let
     val CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...} = cs;
     val nets = [safe0_netpair, safep_netpair, haz_netpair, dup_netpair];
-    val erules = find_erules facts nets;
+    val erules = Data.not_elim :: imp_elim :: find_erules facts nets;
 
     val tac = SUBGOAL (fn (goal, i) =>
       let