tweak
authorpaulson
Fri Sep 26 11:04:21 2003 +0200 (2003-09-26)
changeset 14209180cd69a5dbb
parent 14208 144f45277d5a
child 14210 69e48401da98
tweak
doc-src/Logics/syntax.tex
     1.1 --- a/doc-src/Logics/syntax.tex	Fri Sep 26 10:34:57 2003 +0200
     1.2 +++ b/doc-src/Logics/syntax.tex	Fri Sep 26 11:04:21 2003 +0200
     1.3 @@ -36,9 +36,9 @@
     1.4  syntax $\forall x.t$ to mean $All(\lambda x.t)$.  We can also write $\forall
     1.5  x@1\ldots x@m.t$ to abbreviate $\forall x@1.  \ldots \forall x@m.t$; this is
     1.6  possible for any constant provided that $\tau$ and $\tau'$ are the same type.
     1.7 -HOL's description operator $\varepsilon x.P\,x$ has type $(\alpha\To
     1.8 -bool)\To\alpha$ and can bind only one variable, except when $\alpha$ is
     1.9 -$bool$.  ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a
    1.10 +The Hilbert description operator $\varepsilon x.P\,x$ has type $(\alpha\To
    1.11 +bool)\To\alpha$ and normally binds only one variable.  
    1.12 +ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a
    1.13  binder because it has type $[i, i\To o]\To o$.  The syntax for binders allows
    1.14  type constraints on bound variables, as in
    1.15  \[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \]