# HG changeset patch
# User paulson
# Date 861617789 -7200
# Node ID 8036aaf49f7072d6320f7272f9295fb7eee5c98c
# Parent  c5293a17afa65e32d5c38f2e38d7332a324a12af
New elimination rule for "unique existence"

diff -r c5293a17afa6 -r 8036aaf49f70 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Mon Apr 21 12:16:04 1997 +0200
+++ b/src/HOL/cladata.ML	Mon Apr 21 12:16:29 1997 +0200
@@ -43,8 +43,8 @@
                        addSEs [conjE,disjE,impCE,FalseE,iffE];
 
 (*Quantifier rules*)
-val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
-                     addSEs [exE,ex1E] addEs [allE];
+val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
+                     addSEs [exE] addEs [allE];
 
 exception CS_DATA of claset;
 
@@ -61,6 +61,18 @@
 
 claset := HOL_cs;
 
+(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
+qed_goal "alt_ex1E" thy
+    "[| ?! 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),
+    (Fast_tac 1)]);
+
+AddSEs [alt_ex1E];
 
 (*** Applying BlastFun to create Blast_tac ***)
 structure Blast_Data =