--- 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"