# HG changeset patch
# User lcp
# Date 783860797 -3600
# Node ID be908d8d41ef3b4006a87396cb05738131eaee7d
# Parent  0727f0c0c4f0bfc1c85a827edf131d8ac50d12a6
ZF/upair/theI2: new

diff -r 0727f0c0c4f0 -r be908d8d41ef src/ZF/upair.ML
--- 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))  *)