diff -r 7d8781fc2c8e -r c0ff8f1ebc16 HOL.ML
--- a/HOL.ML	Wed Oct 12 12:06:56 1994 +0100
+++ b/HOL.ML	Thu Oct 13 09:39:15 1994 +0100
@@ -54,6 +54,7 @@
   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
@@ -271,12 +272,19 @@
 
 (** 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"