--- a/src/ZF/upair.ML Thu Nov 03 11:58:16 1994 +0100
+++ b/src/ZF/upair.ML Thu Nov 03 12:06:37 1994 +0100
@@ -187,6 +187,13 @@
(resolve_tac [major RS the_equality2 RS ssubst] 1),
(REPEAT (assume_tac 1)) ]);
+(*Easier to apply than theI: conclusion has only one occurrence of P*)
+val theI2 = prove_goal ZF.thy
+ "[| EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x.P(x))"
+ (fn prems => [ resolve_tac prems 1,
+ rtac theI 1,
+ resolve_tac prems 1 ]);
+
(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then
(THE x.P(x)) rewrites to (THE x. Q(x)) *)