summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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)" |