author wenzelm Fri, 09 May 1997 19:43:16 +0200 changeset 3151 c9a6b415dae6 parent 3150 a8faa68c68b5 child 3152 065c701c7827
minor tuning; add ref to WWW theory lib;
 doc-src/Logics/intro.tex file | annotate | diff | comparison | revisions
--- 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