# HG changeset patch
# User lcp
# Date 785106068 -3600
# Node ID b470cc6326aabc2868a813aa9a530e7153169f18
# Parent  1f5800d2c366854b4217202a52ee229a84d1413a
In ZF, type i has class term, not (just) logic

diff -r 1f5800d2c366 -r b470cc6326aa doc-src/Logics/ZF.tex
--- 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