--- 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"
--- 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 *)