author | wenzelm |
Tue, 18 May 2021 15:17:55 +0200 | |
changeset 73723 | 1bbbaae6b5e3 |
parent 52552 | 0260bdba4dd7 |
permissions | -rw-r--r-- |
7837 | 1 |
\documentclass[12pt,a4paper]{report} |
52552
0260bdba4dd7
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
wenzelm
parents:
48985
diff
changeset
|
2 |
\usepackage{isabelle,isabellesym} |
48942
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
42637
diff
changeset
|
3 |
\usepackage{graphicx,iman,extra,ttbox,proof,latexsym,pdfsetup} |
2661 | 4 |
|
104 | 5 |
%%%STILL NEEDS MODAL, LCF |
349 | 6 |
%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
7 |
%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
|
8 |
%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
|
104 | 9 |
%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
10 |
%% run ../sedindex logics to prepare index file |
|
73723 | 11 |
\title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex] Isabelle's Logics} |
104 | 12 |
|
3131 | 13 |
\author{{\em Lawrence C. Paulson}\\ |
14 |
Computer Laboratory \\ University of Cambridge \\ |
|
15 |
\texttt{lcp@cl.cam.ac.uk}\\[3ex] |
|
16 |
With Contributions by Tobias Nipkow and Markus Wenzel% |
|
7160 | 17 |
\thanks{Markus Wenzel made numerous improvements. Sara Kalvala |
18 |
contributed Chap.\ts\ref{chap:sequents}. Philippe de Groote |
|
9695 | 19 |
wrote the first version of the logic~LK. Tobias Nipkow developed |
20 |
LCF and~Cube. Martin Coen developed~Modal with assistance |
|
7160 | 21 |
from Rajeev Gor\'e. The research has been funded by the EPSRC |
8979 | 22 |
(grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT |
23 |
(projects 3245: Logical Frameworks, and 6453: Types), and by the DFG |
|
24 |
Schwerpunktprogramm \emph{Deduktion}.} } |
|
104 | 25 |
|
26 |
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
|
27 |
\hrule\bigskip} |
|
349 | 28 |
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
104 | 29 |
|
52552
0260bdba4dd7
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
wenzelm
parents:
48985
diff
changeset
|
30 |
\newcommand\bs{\char '134 } % A backslash character for \tt font |
0260bdba4dd7
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
wenzelm
parents:
48985
diff
changeset
|
31 |
|
104 | 32 |
\makeindex |
33 |
||
34 |
\underscoreoff |
|
35 |
||
465 | 36 |
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? |
104 | 37 |
|
38 |
\pagestyle{headings} |
|
39 |
\sloppy |
|
40 |
\binperiod %%%treat . like a binary operator |
|
41 |
||
42 |
\begin{document} |
|
43 |
\maketitle |
|
44 |
\pagenumbering{roman} \tableofcontents \clearfirst |
|
48970
8be091776e93
prefer \input which actually checks file existence;
wenzelm
parents:
48942
diff
changeset
|
45 |
\input{preface} |
8be091776e93
prefer \input which actually checks file existence;
wenzelm
parents:
48942
diff
changeset
|
46 |
\input{syntax} |
52552
0260bdba4dd7
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
wenzelm
parents:
48985
diff
changeset
|
47 |
\input{HOL} |
48970
8be091776e93
prefer \input which actually checks file existence;
wenzelm
parents:
48942
diff
changeset
|
48 |
\input{LK} |
8be091776e93
prefer \input which actually checks file existence;
wenzelm
parents:
48942
diff
changeset
|
49 |
\input{Sequents} |
8be091776e93
prefer \input which actually checks file existence;
wenzelm
parents:
48942
diff
changeset
|
50 |
%%\input{Modal} |
8be091776e93
prefer \input which actually checks file existence;
wenzelm
parents:
48942
diff
changeset
|
51 |
\input{CTT} |
104 | 52 |
\bibliographystyle{plain} |
48942
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
42637
diff
changeset
|
53 |
\bibliography{manual} |
8828 | 54 |
\printindex |
104 | 55 |
\end{document} |