doc-src/Logics/logics.tex
author wenzelm
Mon May 08 11:13:28 2000 +0200 (2000-05-08)
changeset 8828 5be2d1745c61
parent 7837 d4fb2d14edd4
child 8979 802acc97fdaf
permissions -rw-r--r--
improved indexing;
paulson@6072
     1
%% $Id$
wenzelm@7837
     2
\documentclass[12pt,a4paper]{report}
wenzelm@7837
     3
\usepackage{graphicx,../iman,../extra,../proof,../rail,latexsym,../pdfsetup}
wenzelm@2661
     4
lcp@104
     5
%%%STILL NEEDS MODAL, LCF
lcp@349
     6
%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
lcp@349
     7
%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
lcp@349
     8
%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
lcp@104
     9
%%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
lcp@104
    10
%% run    ../sedindex logics    to prepare index file
wenzelm@6623
    11
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Isabelle's Logics}
lcp@104
    12
paulson@3131
    13
\author{{\em Lawrence C. Paulson}\\
paulson@3131
    14
        Computer Laboratory \\ University of Cambridge \\
paulson@3131
    15
        \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
paulson@3131
    16
        With Contributions by Tobias Nipkow and Markus Wenzel%
paulson@7160
    17
 \thanks{Markus Wenzel made numerous improvements.  Sara Kalvala
paulson@7160
    18
    contributed Chap.\ts\ref{chap:sequents}.  Philippe de Groote
paulson@7160
    19
   wrote the first version of the logic~\LK{}.  Tobias Nipkow developed
paulson@7160
    20
   \LCF{} and~\Cube{}.  Martin Coen developed~\Modal{} with assistance
paulson@7160
    21
   from Rajeev Gor\'e.  The research has been funded by the EPSRC
paulson@7160
    22
   (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT
paulson@7160
    23
   project 6453: Types.} }
lcp@104
    24
lcp@104
    25
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
lcp@104
    26
  \hrule\bigskip}
lcp@349
    27
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
lcp@104
    28
lcp@104
    29
\makeindex
lcp@104
    30
lcp@104
    31
\underscoreoff
lcp@104
    32
nipkow@465
    33
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
lcp@104
    34
lcp@104
    35
\pagestyle{headings}
lcp@104
    36
\sloppy
lcp@104
    37
\binperiod     %%%treat . like a binary operator
lcp@104
    38
lcp@104
    39
\begin{document}
lcp@104
    40
\maketitle 
lcp@104
    41
\pagenumbering{roman} \tableofcontents \clearfirst
paulson@6072
    42
\include{preface}
paulson@6072
    43
\include{syntax}
lcp@104
    44
\include{LK}
paulson@7160
    45
\include{Sequents}
lcp@104
    46
%%\include{Modal}
lcp@104
    47
\include{CTT}
lcp@104
    48
\bibliographystyle{plain}
paulson@6592
    49
\bibliography{../manual}
wenzelm@8828
    50
\printindex
lcp@104
    51
\end{document}