src/ZF/ZF.thy
changeset 63901 4ce989e962e0
parent 62149 a02b79ef2339
child 65386 e3fb3036a00e
equal deleted inserted replaced
63899:dc036b1a2a6f 63901:4ce989e962e0
    47 
    47 
    48 (* Derived form of replacement, restricting P to its functional part.
    48 (* Derived form of replacement, restricting P to its functional part.
    49    The resulting set (for functional P) is the same as with
    49    The resulting set (for functional P) is the same as with
    50    PrimReplace, but the rules are simpler. *)
    50    PrimReplace, but the rules are simpler. *)
    51 definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
    51 definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
    52   where "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
    52   where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
    53 
    53 
    54 syntax
    54 syntax
    55   "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
    55   "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
    56 translations
    56 translations
    57   "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
    57   "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"