summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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;

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