19 |
19 |
20 \author{{\em Lawrence C. Paulson}\\ |
20 \author{{\em Lawrence C. Paulson}\\ |
21 Computer Laboratory \\ University of Cambridge \\ |
21 Computer Laboratory \\ University of Cambridge \\ |
22 \texttt{lcp@cl.cam.ac.uk}\\[3ex] |
22 \texttt{lcp@cl.cam.ac.uk}\\[3ex] |
23 With Contributions by Tobias Nipkow and Markus Wenzel% |
23 With Contributions by Tobias Nipkow and Markus Wenzel% |
24 \thanks{Tobias Nipkow revised and extended |
24 \thanks{Markus Wenzel made numerous improvements. Philippe de Groote |
25 the chapter on \HOL. Markus Wenzel made numerous improvements. |
25 wrote the first version of the logic~\LK{}. Tobias Nipkow developed |
26 Philippe de Groote wrote the |
26 \LCF{} and~\Cube{}. Martin Coen developed~\Modal{} with assistance |
27 first version of the logic~\LK{}. Tobias |
27 from Rajeev Gor\'e. The research has been funded by the EPSRC |
28 Nipkow developed~\HOL{}, \LCF{} and~\Cube{}. Martin Coen |
28 (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT |
29 developed~\Modal{} with assistance from Rajeev Gor\'e. The research has |
29 project 6453: Types.} } |
30 been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381, |
|
31 GR/K77051) and by ESPRIT project 6453: Types.} |
|
32 } |
|
33 |
30 |
34 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
31 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
35 \hrule\bigskip} |
32 \hrule\bigskip} |
36 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
33 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
37 |
34 |
48 \begin{document} |
45 \begin{document} |
49 \maketitle |
46 \maketitle |
50 \pagenumbering{roman} \tableofcontents \clearfirst |
47 \pagenumbering{roman} \tableofcontents \clearfirst |
51 \include{preface} |
48 \include{preface} |
52 \include{syntax} |
49 \include{syntax} |
53 \include{HOL} |
|
54 \include{LK} |
50 \include{LK} |
55 %%\include{Modal} |
51 %%\include{Modal} |
56 \include{CTT} |
52 \include{CTT} |
57 %%\include{Cube} |
53 %%\include{Cube} |
58 %%\include{LCF} |
54 %%\include{LCF} |
59 \bibliographystyle{plain} |
55 \bibliographystyle{plain} |
60 \bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref} |
56 \bibliography{bib,string,general,atp,theory,funprog,logicprog,isabelle,crossref} |
61 \input{logics.ind} |
57 \input{logics.ind} |
62 \end{document} |
58 \end{document} |