src/ZF/ZF.thy

  (* ZF axioms -- see Suppes p.238
     Axioms for Union, Pow and Replace state existence only,
         uniqueness is derivable using extensionality.  *)
 
 extension       "A = B <-> A <= B & B <= A"
-union_iff       "A : Union(C) <-> (EX B:C. A:B)"
-power_set       "A : Pow(B) <-> A <= B"
+Union_iff       "A : Union(C) <-> (EX B:C. A:B)"
+Pow_iff         "A : Pow(B) <-> A <= B"
 succ_def        "succ(i) == cons(i,i)"
 
  (*We may name this set, though it is not uniquely defined. *)
 infinity        "0:Inf & (ALL y:Inf. succ(y): Inf)"