author | clasohm |
Tue, 09 May 1995 10:43:19 +0200 | |
changeset 1113 | dd7284573601 |
parent 873 | 0cfc734e3dbd |
child 1186 | 906c32af858d |
permissions | -rw-r--r-- |
463 | 1 |
\documentstyle[a4,12pt,proof,iman,extra,rail]{report} |
104 | 2 |
%% $Id$ |
3 |
%%%STILL NEEDS MODAL, LCF |
|
111 | 4 |
%%%\includeonly{ZF} |
349 | 5 |
%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
6 |
%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
|
7 |
%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
|
104 | 8 |
%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
9 |
%% run ../sedindex logics to prepare index file |
|
10 |
\title{Isabelle's Object-Logics} |
|
11 |
||
317 | 12 |
\author{{\em Lawrence C. Paulson}\thanks{Tobias Nipkow and Markus Wenzel |
13 |
suggested changes and corrections. Philippe de Groote wrote the |
|
104 | 14 |
first version of the logic~\LK{} and contributed to~\ZF{}. Tobias |
15 |
Nipkow developed~\HOL{}, \LCF{} and~\Cube{}. Philippe No\"el and |
|
16 |
Martin Coen made many contributions to~\ZF{}. Martin Coen |
|
17 |
developed~\Modal{} with assistance from Rajeev Gor\'e. The research |
|
18 |
has been funded by the SERC (grants GR/G53279, GR/H40570) and by ESPRIT |
|
349 | 19 |
project 6453: Types.}\\ |
104 | 20 |
Computer Laboratory \\ |
21 |
University of Cambridge \\[2ex] |
|
22 |
{\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} \\[3cm] |
|
23 |
{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson} } |
|
24 |
||
25 |
\date{} |
|
26 |
||
27 |
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
|
28 |
\hrule\bigskip} |
|
349 | 29 |
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
104 | 30 |
|
31 |
\makeindex |
|
32 |
||
287 | 33 |
%%\newenvironment{example}{\begin{Example}\rm}{\end{Example}} |
34 |
%%\newtheorem{Example}{Example}[chapter] |
|
35 |
||
104 | 36 |
\underscoreoff |
37 |
||
465 | 38 |
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? |
104 | 39 |
|
40 |
\pagestyle{headings} |
|
41 |
\sloppy |
|
42 |
\binperiod %%%treat . like a binary operator |
|
43 |
||
44 |
\begin{document} |
|
45 |
\maketitle |
|
46 |
\pagenumbering{roman} \tableofcontents \clearfirst |
|
47 |
\include{intro} |
|
48 |
\include{FOL} |
|
49 |
\include{ZF} |
|
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
873
diff
changeset
|
50 |
\include{CHOL} |
104 | 51 |
\include{LK} |
52 |
%%\include{Modal} |
|
53 |
\include{CTT} |
|
54 |
%%\include{Cube} |
|
55 |
%%\include{LCF} |
|
56 |
\bibliographystyle{plain} |
|
873 | 57 |
\bibliography{string,atp,theory,funprog,logicprog,isabelle,crossref} |
104 | 58 |
\input{logics.ind} |
59 |
\end{document} |