src/ZF/upair.ML
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 ***)