# HG changeset patch
# User nipkow
# Date 964195914 -7200
# Node ID 99476cf93dad55db90c7e49856ffc99e4fe95176
# Parent  aad13b59b8d9351e7862a049e71f1e7daeba04b9
added ex_someI

diff -r aad13b59b8d9 -r 99476cf93dad src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Fri Jul 21 18:01:36 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Fri Jul 21 18:11:54 2000 +0200
@@ -355,6 +355,12 @@
 (** Select: Hilbert's Epsilon-operator **)
 section "@";
 
+(*Easier to apply than selectI if witness ?a comes from an EX-formula*)
+Goal "EX a. P a ==> P (SOME x. P x)";
+by (etac exE 1);
+by (etac selectI 1);
+qed "ex_someI";
+
 (*Easier to apply than selectI: conclusion has only one occurrence of P*)
 val prems = Goal
     "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)";