diff -r a8faa68c68b5 -r c9a6b415dae6 doc-src/Logics/intro.tex
--- a/doc-src/Logics/intro.tex	Fri May 09 19:42:09 1997 +0200
+++ b/doc-src/Logics/intro.tex	Fri May 09 19:43:16 1997 +0200
@@ -41,12 +41,16 @@
 
 \item[\thydx{Cube}] is Barendregt's $\lambda$-cube.
 \end{ttdescription}
-The logics {\tt CCL}, {\tt LCF}, {\tt HOLCF}, {\tt Modal} and {\tt Cube}
-are currently undocumented.
+The logics {\tt CCL}, {\tt LCF}, {\tt HOLCF}, {\tt Modal} and {\tt
+  Cube} are currently undocumented. All object-logics' sources are
+distributed with Isabelle (see the directory \texttt{src}).  They are
+also available for browsing on the WWW at
+\texttt{http://www4.informatik.tu-muenchen.de/\~\relax
+  nipkow/isabelle/}.
 
-You should not read this before reading {\em Introduction to Isabelle\/}
-and performing some Isabelle proofs.  Consult the {\em Reference Manual}
-for more information on tactics, packages, etc.
+You should not read this manual before reading {\em Introduction to
+  Isabelle\/} and performing some Isabelle proofs.  Consult the {\em
+  Reference Manual} for more information on tactics, packages, etc.
 
 
 \section{Syntax definitions}
@@ -90,7 +94,7 @@
 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. R(x,y) \]
+\[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \]
 
 To avoid excess detail, the logic descriptions adopt a semi-formal style.
 Infix operators and binding operators are listed in separate tables, which