|
1 %% $Id$ |
1 \documentclass[12pt]{report} |
2 \documentclass[12pt]{report} |
2 \usepackage{graphicx,a4,latexsym,../pdfsetup} |
3 \usepackage{graphicx,a4,latexsym,../pdfsetup} |
3 |
4 |
4 \makeatletter |
5 \makeatletter |
5 \input{../proof.sty} |
6 \input{../proof.sty} |
6 \input{../rail.sty} |
7 \input{../rail.sty} |
7 \input{../iman.sty} |
8 \input{../iman.sty} |
8 \input{../extra.sty} |
9 \input{../extra.sty} |
9 \makeatother |
10 \makeatother |
10 |
11 |
11 %% $Id$ |
|
12 %%%STILL NEEDS MODAL, LCF |
12 %%%STILL NEEDS MODAL, LCF |
13 %%%\includeonly{ZF} |
|
14 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
13 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
15 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
14 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
16 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
15 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
17 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
16 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
18 %% run ../sedindex logics to prepare index file |
17 %% run ../sedindex logics to prepare index file |
19 \title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Isabelle's Object-Logics} |
18 \title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Isabelle's Logics} |
20 |
19 |
21 \author{{\em Lawrence C. Paulson}\\ |
20 \author{{\em Lawrence C. Paulson}\\ |
22 Computer Laboratory \\ University of Cambridge \\ |
21 Computer Laboratory \\ University of Cambridge \\ |
23 \texttt{lcp@cl.cam.ac.uk}\\[3ex] |
22 \texttt{lcp@cl.cam.ac.uk}\\[3ex] |
24 With Contributions by Tobias Nipkow and Markus Wenzel% |
23 With Contributions by Tobias Nipkow and Markus Wenzel% |
25 \thanks{Tobias Nipkow revised and extended |
24 \thanks{Tobias Nipkow revised and extended |
26 the chapter on \HOL. Markus Wenzel made numerous improvements. |
25 the chapter on \HOL. Markus Wenzel made numerous improvements. |
27 Philippe de Groote wrote the |
26 Philippe de Groote wrote the |
28 first version of the logic~\LK{} and contributed to~\ZF{}. Tobias |
27 first version of the logic~\LK{}. Tobias |
29 Nipkow developed~\HOL{}, \LCF{} and~\Cube{}. Philippe No\"el and |
28 Nipkow developed~\HOL{}, \LCF{} and~\Cube{}. Martin Coen |
30 Martin Coen made many contributions to~\ZF{}. Martin Coen |
|
31 developed~\Modal{} with assistance from Rajeev Gor\'e. The research has |
29 developed~\Modal{} with assistance from Rajeev Gor\'e. The research has |
32 been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381, |
30 been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381, |
33 GR/K77051) and by ESPRIT project 6453: Types.} |
31 GR/K77051) and by ESPRIT project 6453: Types.} |
34 } |
32 } |
35 |
33 |
36 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
34 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
37 \hrule\bigskip} |
35 \hrule\bigskip} |
38 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
36 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
39 |
37 |
40 \makeindex |
38 \makeindex |
41 |
|
42 %%\newenvironment{example}{\begin{Example}\rm}{\end{Example}} |
|
43 %%\newtheorem{Example}{Example}[chapter] |
|
44 |
39 |
45 \underscoreoff |
40 \underscoreoff |
46 |
41 |
47 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? |
42 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? |
48 |
43 |