doc-src/Logics/intro.tex
 changeset 3151 c9a6b415dae6 parent 3139 671a5f2cac6a child 3216 fdcb907f9c93
--- 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/}.

-and performing some Isabelle proofs.  Consult the {\em Reference Manual}
+  Isabelle\/} and performing some Isabelle proofs.  Consult the {\em
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
-$\forall (x{::}\alpha) \; y{::}\beta. R(x,y)$
+$\forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z)$
Infix operators and binding operators are listed in separate tables, which