diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/ZF.thy	Tue Jul 26 13:44:42 1994 +0200
@@ -133,8 +133,8 @@
         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. *)