Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
single method: include not_elim, imp_elim;
authorwenzelm
Thu, 22 Apr 1999 18:23:45 +0200
changeset 6489 e02c5290885d
parent 6488 271969bb7f95
child 6490 4961ecbaaff7
single method: include not_elim, imp_elim;
src/Provers/classical.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle