changeset 5242 | 3087dafb70ec |
parent 5116 | 8eb343ab5748 |
child 5325 | f7a5e06adea1 |
--- a/src/ZF/upair.ML Tue Aug 04 16:05:19 1998 +0200 +++ b/src/ZF/upair.ML Tue Aug 04 16:06:55 1998 +0200 @@ -16,7 +16,7 @@ val Pow_bottom = empty_subsetI RS PowI; (* 0 : Pow(B) *) val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) -val Pow_neq_0 = Pow_top RSN (2,equals0D); (* Pow(a)=0 ==> P *) +val Pow_neq_0 = Pow_top RSN (2,equals0E); (* Pow(a)=0 ==> P *) (*** Unordered pairs - Upair ***)