src/ZF/ZF.thy
changeset 63901 4ce989e962e0
parent 62149 a02b79ef2339
child 65386 e3fb3036a00e
     1.1 --- a/src/ZF/ZF.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/ZF/ZF.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4     The resulting set (for functional P) is the same as with
     1.5     PrimReplace, but the rules are simpler. *)
     1.6  definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
     1.7 -  where "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
     1.8 +  where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
     1.9  
    1.10  syntax
    1.11    "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")