--- 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