HOL.ML

   val notE	: thm
   val notI	: thm
   val notnotD 	: thm
   val rev_mp	: thm
   val select_equality	: thm
+  val selectI2	: thm
   val spec	: thm
   val sstac	: thm list -> int -> tactic
   val ssubst	: thm
   val stac	: thm -> int -> tactic
   val strip_tac	: int -> tactic

   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
 
 
 (** Select: Hilbert's Epsilon-operator **)
 
-val select_equality = prove_goal HOL.thy
-    "[| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a"
+(*Easier to apply than selectI: conclusion has only one occurrence of P*)
+val selectI2 = prove_goal HOL.thy
+    "[| P(a);  !!x. P(x) ==> Q(x) |] ==> Q(@x.P(x))"
  (fn prems => [ resolve_tac prems 1, 
 	        rtac selectI 1, 
 		resolve_tac prems 1 ]);
+
+val select_equality = prove_goal HOL.thy
+    "[| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a"
+ (fn prems => [ rtac selectI2 1, 
+		REPEAT (ares_tac prems 1) ]);
+
 
 (** Classical intro rules for disjunction and existential quantifiers *)
 
 val disjCI = prove_goal HOL.thy "(~Q ==> P) ==> P|Q"
  (fn prems=>