# HG changeset patch
# User berghofe
# Date 901279643 -7200
# Node ID d1067e2c3f9f1f9bcdf9c1e3b6497cd51cc67ca7
# Parent  9b8547a9496afa9c74bd507626d698437c36684e
Added theorem ex1_implies_ex.

diff -r 9b8547a9496a -r d1067e2c3f9f src/HOL/HOL.ML
--- 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 "@";