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

doc-src/ZF/ZF.tex

changeset 6745 | 74e8f703f5f2 |

parent 6592 | c120262044b6 |

child 8249 | 3fc32155372c |

equal
deleted
inserted
replaced

6744:9727e83f0578 | 6745:74e8f703f5f2 |
---|---|

1171 set (Fig.\ts\ref{zf-fixedpt}). The theory defines least and greatest |
1171 set (Fig.\ts\ref{zf-fixedpt}). The theory defines least and greatest |

1172 fixedpoint operators with corresponding induction and coinduction rules. |
1172 fixedpoint operators with corresponding induction and coinduction rules. |

1173 These are essential to many definitions that follow, including the natural |
1173 These are essential to many definitions that follow, including the natural |

1174 numbers and the transitive closure operator. The (co)inductive definition |
1174 numbers and the transitive closure operator. The (co)inductive definition |

1175 package also uses the fixedpoint operators~\cite{paulson-CADE}. See |
1175 package also uses the fixedpoint operators~\cite{paulson-CADE}. See |

1176 Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski |
1176 Davey and Priestley~\cite{davey-priestley} for more on the Knaster-Tarski |

1177 Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle |
1177 Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle |

1178 proofs. |
1178 proofs. |

1179 |
1179 |

1180 Monotonicity properties are proved for most of the set-forming operations: |
1180 Monotonicity properties are proved for most of the set-forming operations: |

1181 union, intersection, Cartesian product, image, domain, range, etc. These |
1181 union, intersection, Cartesian product, image, domain, range, etc. These |