diff -r 13f3aaf12be2 -r ec7d7f877712 doc-src/Logics/syntax.tex
--- a/doc-src/Logics/syntax.tex	Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/Logics/syntax.tex	Mon Aug 28 13:52:38 2000 +0200
@@ -31,16 +31,15 @@
 becomes syntactically invalid if the brackets are removed.
 
 A {\bf binder} is a symbol associated with a constant of type
-$(\sigma\To\tau)\To\tau'$.  For instance, we may declare~$\forall$ as
-a binder for the constant~$All$, which has type $(\alpha\To o)\To o$.
-This defines the syntax $\forall x.t$ to mean $All(\lambda x.t)$.  We
-can also write $\forall x@1\ldots x@m.t$ to abbreviate $\forall x@1.
-\ldots \forall x@m.t$; this is possible for any constant provided that
-$\tau$ and $\tau'$ are the same type.  \HOL's description operator
-$\varepsilon x.P\,x$ has type $(\alpha\To bool)\To\alpha$ and can bind
-only one variable, except when $\alpha$ is $bool$.  \ZF's bounded
-quantifier $\forall x\in A.P(x)$ cannot be declared as a binder
-because it has type $[i, i\To o]\To o$.  The syntax for binders allows
+$(\sigma\To\tau)\To\tau'$.  For instance, we may declare~$\forall$ as a binder
+for the constant~$All$, which has type $(\alpha\To o)\To o$.  This defines the
+syntax $\forall x.t$ to mean $All(\lambda x.t)$.  We can also write $\forall
+x@1\ldots x@m.t$ to abbreviate $\forall x@1.  \ldots \forall x@m.t$; this is
+possible for any constant provided that $\tau$ and $\tau'$ are the same type.
+HOL's description operator $\varepsilon x.P\,x$ has type $(\alpha\To
+bool)\To\alpha$ and can bind only one variable, except when $\alpha$ is
+$bool$.  ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a
+binder because it has type $[i, i\To o]\To o$.  The syntax for binders allows
 type constraints on bound variables, as in
 \[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \]