# HG changeset patch
# User nipkow
# Date 1189180563 -7200
# Node ID 9b19da7b2b08fa3d54172fe5bf34e0f2d2b6b206
# Parent  bb7fdd10de9a534f56c0fedcd614e336181c5cee
added lemma

diff -r bb7fdd10de9a -r 9b19da7b2b08 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Sep 07 15:35:25 2007 +0200
+++ b/src/HOL/HOL.thy	Fri Sep 07 17:56:03 2007 +0200
@@ -708,6 +708,10 @@
   shows "Q (THE x. P x)"
 by (iprover intro: assms theI)
 
+lemma the1I2: assumes "EX! x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
+by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
+           elim:allE impE)
+
 lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
 apply (rule the_equality)
 apply  assumption