src/ZF/upair.thy
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"