# HG changeset patch
# User wenzelm
# Date 911220875 -3600
# Node ID b3548f939dd2a72a5970f283172e554bef2d77ed
# Parent  4a75d89e281811ecbdd7b4d64ab2e305a5f69833
removed genelim.ML;

diff -r 4a75d89e2818 -r b3548f939dd2 src/Provers/README
--- a/src/Provers/README	Mon Nov 16 11:33:42 1998 +0100
+++ b/src/Provers/README	Mon Nov 16 13:54:35 1998 +0100
@@ -8,7 +8,6 @@
   blast.ML              generic tableau prover with proof reconstruction
   clasimp.ML		combination of classical reasoner and simplifier
   classical.ML          theorem prover for classical logics
-  genelim.ML            bits and pieces for deriving elimination rules
   hypsubst.ML           tactic to substitute in the hypotheses
   ind.ML                a simple induction package
   quantifier1.ML	simplification procedures for "1 point rules"
diff -r 4a75d89e2818 -r b3548f939dd2 src/Provers/genelim.ML
--- a/src/Provers/genelim.ML	Mon Nov 16 11:33:42 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(** Generalized elimination rules **)
-
-(*Generalized elimination for two conclusions*)
-val prems = goal proto_pure_thy 
-     "[| PROP U ==> PROP VA;  \
-\        PROP U ==> PROP VB;  \
-\        PROP U;              \
-\        [| PROP VA; PROP VB |] ==> PROP W    \
-\     |] ==> PROP W";
-by (REPEAT (resolve_tac prems 1));
-val general_elim2_rl = result();
-
-fun make_elim2 (rl1,rl2) = standard (rl2 COMP rl1 COMP general_elim2_rl);
-fun elim2_tac (rl1,rl2) = eresolve_tac [rl2 COMP rl1 COMP general_elim2_rl];
-
-
-(*For example,  make_elim2(conjunct1,conjunct2)  
-  yields conjunction elimination *)