author | paulson |
Fri, 08 Jan 1999 14:02:04 +0100 | |
changeset 6072 | 5583261db33d |
parent 5170 | 33fbffd06c12 |
child 6582 | 75f31d45fb8b |
permissions | -rw-r--r-- |
6072 | 1 |
%% $Id$ |
3096 | 2 |
\documentclass[12pt]{report} |
5165 | 3 |
\usepackage{graphicx,a4,latexsym,../pdfsetup} |
3096 | 4 |
|
2661 | 5 |
\makeatletter |
3287 | 6 |
\input{../proof.sty} |
2661 | 7 |
\input{../rail.sty} |
8 |
\input{../iman.sty} |
|
9 |
\input{../extra.sty} |
|
10 |
\makeatother |
|
11 |
||
104 | 12 |
%%%STILL NEEDS MODAL, LCF |
349 | 13 |
%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
14 |
%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
|
15 |
%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
|
104 | 16 |
%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
17 |
%% run ../sedindex logics to prepare index file |
|
6072 | 18 |
\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Isabelle's Logics} |
104 | 19 |
|
3131 | 20 |
\author{{\em Lawrence C. Paulson}\\ |
21 |
Computer Laboratory \\ University of Cambridge \\ |
|
22 |
\texttt{lcp@cl.cam.ac.uk}\\[3ex] |
|
23 |
With Contributions by Tobias Nipkow and Markus Wenzel% |
|
24 |
\thanks{Tobias Nipkow revised and extended |
|
25 |
the chapter on \HOL. Markus Wenzel made numerous improvements. |
|
3005 | 26 |
Philippe de Groote wrote the |
6072 | 27 |
first version of the logic~\LK{}. Tobias |
28 |
Nipkow developed~\HOL{}, \LCF{} and~\Cube{}. Martin Coen |
|
3131 | 29 |
developed~\Modal{} with assistance from Rajeev Gor\'e. The research has |
30 |
been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381, |
|
31 |
GR/K77051) and by ESPRIT project 6453: Types.} |
|
32 |
} |
|
104 | 33 |
|
34 |
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
|
35 |
\hrule\bigskip} |
|
349 | 36 |
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
104 | 37 |
|
38 |
\makeindex |
|
39 |
||
40 |
\underscoreoff |
|
41 |
||
465 | 42 |
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? |
104 | 43 |
|
44 |
\pagestyle{headings} |
|
45 |
\sloppy |
|
46 |
\binperiod %%%treat . like a binary operator |
|
47 |
||
48 |
\begin{document} |
|
49 |
\maketitle |
|
50 |
\pagenumbering{roman} \tableofcontents \clearfirst |
|
6072 | 51 |
\include{preface} |
52 |
\include{syntax} |
|
1226 | 53 |
\include{HOL} |
104 | 54 |
\include{LK} |
55 |
%%\include{Modal} |
|
56 |
\include{CTT} |
|
57 |
%%\include{Cube} |
|
58 |
%%\include{LCF} |
|
59 |
\bibliographystyle{plain} |
|
2933
f842a75d9624
Updated discussion and references for inductive definitions
paulson
parents:
2661
diff
changeset
|
60 |
\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref} |
104 | 61 |
\input{logics.ind} |
62 |
\end{document} |