changeset 14883 | ca000a495448 |
parent 14153 | 76a6ba67bd15 |
child 15091 | 77d160469390 |
--- a/src/ZF/upair.thy Sun Jun 06 18:36:36 2004 +0200 +++ b/src/ZF/upair.thy Tue Jun 08 16:22:30 2004 +0200 @@ -147,7 +147,7 @@ lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!] -subsection{*Rules for Descriptions*} +subsection{*Descriptions*} lemma the_equality [intro]: "[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"