39 \item[\thydx{Modal}] implements the modal logics $T$, $S4$, |
39 \item[\thydx{Modal}] implements the modal logics $T$, $S4$, |
40 and~$S43$. It is built upon~\LK{}. |
40 and~$S43$. It is built upon~\LK{}. |
41 |
41 |
42 \item[\thydx{Cube}] is Barendregt's $\lambda$-cube. |
42 \item[\thydx{Cube}] is Barendregt's $\lambda$-cube. |
43 \end{ttdescription} |
43 \end{ttdescription} |
44 The logics {\tt CCL}, {\tt LCF}, {\tt HOLCF}, {\tt Modal} and {\tt Cube} |
44 The logics {\tt CCL}, {\tt LCF}, {\tt HOLCF}, {\tt Modal} and {\tt |
45 are currently undocumented. |
45 Cube} are currently undocumented. All object-logics' sources are |
|
46 distributed with Isabelle (see the directory \texttt{src}). They are |
|
47 also available for browsing on the WWW at |
|
48 \texttt{http://www4.informatik.tu-muenchen.de/\~\relax |
|
49 nipkow/isabelle/}. |
46 |
50 |
47 You should not read this before reading {\em Introduction to Isabelle\/} |
51 You should not read this manual before reading {\em Introduction to |
48 and performing some Isabelle proofs. Consult the {\em Reference Manual} |
52 Isabelle\/} and performing some Isabelle proofs. Consult the {\em |
49 for more information on tactics, packages, etc. |
53 Reference Manual} for more information on tactics, packages, etc. |
50 |
54 |
51 |
55 |
52 \section{Syntax definitions} |
56 \section{Syntax definitions} |
53 The syntax of each logic is presented using a context-free grammar. |
57 The syntax of each logic is presented using a context-free grammar. |
54 These grammars obey the following conventions: |
58 These grammars obey the following conventions: |
88 $\varepsilon x.P\,x$ has type $(\alpha\To bool)\To\alpha$ and can bind |
92 $\varepsilon x.P\,x$ has type $(\alpha\To bool)\To\alpha$ and can bind |
89 only one variable, except when $\alpha$ is $bool$. \ZF's bounded |
93 only one variable, except when $\alpha$ is $bool$. \ZF's bounded |
90 quantifier $\forall x\in A.P(x)$ cannot be declared as a binder |
94 quantifier $\forall x\in A.P(x)$ cannot be declared as a binder |
91 because it has type $[i, i\To o]\To o$. The syntax for binders allows |
95 because it has type $[i, i\To o]\To o$. The syntax for binders allows |
92 type constraints on bound variables, as in |
96 type constraints on bound variables, as in |
93 \[ \forall (x{::}\alpha) \; y{::}\beta. R(x,y) \] |
97 \[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \] |
94 |
98 |
95 To avoid excess detail, the logic descriptions adopt a semi-formal style. |
99 To avoid excess detail, the logic descriptions adopt a semi-formal style. |
96 Infix operators and binding operators are listed in separate tables, which |
100 Infix operators and binding operators are listed in separate tables, which |
97 include their priorities. Grammar descriptions do not include numeric |
101 include their priorities. Grammar descriptions do not include numeric |
98 priorities; instead, the rules appear in order of decreasing priority. |
102 priorities; instead, the rules appear in order of decreasing priority. |