summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Thu, 17 Nov 1994 22:01:08 +0100 | |

changeset 713 | b470cc6326aa |

parent 712 | 1f5800d2c366 |

child 714 | 015ec0a9563a |

In ZF, type i has class term, not (just) logic

--- a/doc-src/Logics/ZF.tex Mon Nov 14 14:47:20 1994 +0100 +++ b/doc-src/Logics/ZF.tex Thu Nov 17 22:01:08 1994 +0100 @@ -135,8 +135,8 @@ the constructs of \FOL. Set theory does not use polymorphism. All terms in {\ZF} have -type~\tydx{i}, which is the type of individuals and lies in class~{\tt - logic}. The type of first-order formulae, remember, is~{\tt o}. +type~\tydx{i}, which is the type of individuals and has class~{\tt + term}. The type of first-order formulae, remember, is~{\tt o}. Infix operators include binary union and intersection ($A\union B$ and $A\inter B$), set difference ($A-B$), and the subset and membership