# HG changeset patch
# User paulson
# Date 861617764 -7200
# Node ID c5293a17afa65e32d5c38f2e38d7332a324a12af
# Parent  223e5d65faaa4e4fda1153b205bea7bdf9f6dcd2
New introduction rule for "unique existence"

diff -r 223e5d65faaa -r c5293a17afa6 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Mon Apr 21 11:19:28 1997 +0200
+++ b/src/HOL/HOL.ML	Mon Apr 21 12:16:04 1997 +0200
@@ -235,6 +235,12 @@
  (fn prems =>
   [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
 
+(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
+qed_goal "ex_ex1I" HOL.thy
+    "[| ? x.P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
+ (fn [ex,eq] => [ (rtac (ex RS exE) 1),
+                  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
+
 qed_goalw "ex1E" HOL.thy [Ex1_def]
     "[| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
  (fn major::prems =>