--- a/src/ZF/ZF.thy Fri Sep 16 18:09:13 2016 +0200
+++ b/src/ZF/ZF.thy Fri Sep 16 21:28:09 2016 +0200
@@ -49,7 +49,7 @@
The resulting set (for functional P) is the same as with
PrimReplace, but the rules are simpler. *)
definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
- where "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
+ where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
syntax
"_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")