changeset 24553 | 9b19da7b2b08 |
parent 24506 | 020db6ec334a |
child 24633 | 0a3a02066244 |
--- 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