doc-src/Logics/CTT.tex
changeset 6072 5583261db33d
parent 5151 1e944fe5ce96
child 6170 9a59cf8ae9b5
     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}