Added theorem ex1_implies_ex.

--- a/src/HOL/HOL.ML	Fri Jul 24 13:19:38 1998 +0200
+++ b/src/HOL/HOL.ML	Fri Jul 24 13:27:23 1998 +0200
@@ -250,6 +250,12 @@
  (fn major::prems =>
   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
 
+Goal "?! x. P x ==> ? x. P x";
+be ex1E 1;
+br exI 1;
+ba 1;
+qed "ex1_implies_ex";
+
 
 (** Select: Hilbert's Epsilon-operator **)
 section "@";