1.1 --- a/doc-src/Logics/CTT.tex Fri Jan 08 13:20:59 1999 +0100
1.2 +++ b/doc-src/Logics/CTT.tex Fri Jan 08 14:02:04 1999 +0100
1.3 @@ -178,10 +178,10 @@
1.4 the one-element type is $T$; other finite types are built as $T+T+T$, etc.
1.5
1.6 \index{*SUM symbol}\index{*PROD symbol}
1.7 -Quantification is expressed using general sums $\sum@{x\in A}B[x]$ and
1.8 +Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
1.9 products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt
1.10 - Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$. $B[x]$} and \hbox{\tt
1.11 - PROD $x$:$A$. $B[x]$}. For example, we may write
1.12 + Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt
1.13 + PROD $x$:$A$.\ $B[x]$}. For example, we may write
1.14 \begin{ttbox}
1.15 SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, \%y. Prod(A, \%x. C(x,y)))
1.16 \end{ttbox}