# HG changeset patch
# User paulson
# Date 1064567061 -7200
# Node ID 180cd69a5dbbde0ac30580b3edcdc5c5ae90007b
# Parent  144f45277d5a8c37d6bed25d1c936a5f9e424548
tweak

diff -r 144f45277d5a -r 180cd69a5dbb doc-src/Logics/syntax.tex
--- a/doc-src/Logics/syntax.tex	Fri Sep 26 10:34:57 2003 +0200
+++ b/doc-src/Logics/syntax.tex	Fri Sep 26 11:04:21 2003 +0200
@@ -36,9 +36,9 @@
 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
+The Hilbert description operator $\varepsilon x.P\,x$ has type $(\alpha\To
+bool)\To\alpha$ and normally binds only one variable.  
+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) \]