src/HOL/HOL.ML
changeset 3003 c5293a17afa6
parent 2562 d571d6660240
child 3436 d68dbb8f22d3
--- 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 =>