src/HOL/HOL.ML
changeset 3436 d68dbb8f22d3
parent 3003 c5293a17afa6
child 3615 e5322197cfea
--- a/src/HOL/HOL.ML	Fri Jun 13 10:04:37 1997 +0200
+++ b/src/HOL/HOL.ML	Fri Jun 13 10:35:13 1997 +0200
@@ -262,6 +262,11 @@
  (fn prems => [ rtac selectI2 1, 
                 REPEAT (ares_tac prems 1) ]);
 
+(*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
+qed_goal "selectI2EX" HOL.thy
+  "[| ? a.P a; !!x. P x ==> Q x |] ==> Q(Eps P)"
+(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
+
 qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (fn prems => [
         rtac iffI 1,
         etac exI 1,