--- a/src/FOL/cladata.ML Thu Mar 27 10:06:36 1997 +0100
+++ b/src/FOL/cladata.ML Thu Mar 27 10:07:11 1997 +0100
@@ -10,6 +10,7 @@
(** Applying HypsubstFun to generate hyp_subst_tac **)
section "Classical Reasoner";
+
(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct
@@ -23,6 +24,18 @@
structure Cla = ClassicalFun(Classical_Data);
open Cla;
+(*Better for fast_tac: needs no quantifier duplication!*)
+qed_goal "alt_ex1E" IFOL.thy
+ "[| EX! x.P(x); \
+\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \
+\ |] ==> R"
+ (fn major::prems =>
+ [ (rtac (major RS ex1E) 1),
+ (REPEAT (ares_tac (allI::prems) 1)),
+ (etac (dup_elim allE) 1),
+ (IntPr.fast_tac 1)]);
+
+
(*Propositional rules
-- iffCE might seem better, but in the examples in ex/cla
run about 7% slower than with iffE*)
@@ -30,8 +43,8 @@
addSEs [conjE,disjE,impCE,FalseE,iffE];
(*Quantifier rules*)
-val FOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
- addSEs [exE,ex1E] addEs [allE];
+val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI]
+ addSEs [exE,alt_ex1E] addEs [allE];
exception CS_DATA of claset;