summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/Logics/syntax.tex

changeset 14209 | 180cd69a5dbb |

parent 9695 | ec7d7f877712 |

child 42637 | 381fdcab0f36 |

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) \]