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