doc-src/Logics/logics.tex
author haftmann
Wed Dec 27 19:10:06 2006 +0100 (2006-12-27)
changeset 21915 4e63c55f4cb4
parent 9695 ec7d7f877712
child 42636 41dff1b862bf
permissions -rw-r--r--
different handling of type variable names
     1 %% $Id$
     2 \documentclass[12pt,a4paper]{report}
     3 \usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,latexsym,../pdfsetup}
     4 
     5 %%%STILL NEEDS MODAL, LCF
     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}  
     9 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
    10 %% run    ../sedindex logics    to prepare index file
    11 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Isabelle's Logics}
    12 
    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%
    17  \thanks{Markus Wenzel made numerous improvements.  Sara Kalvala
    18     contributed Chap.\ts\ref{chap:sequents}.  Philippe de Groote
    19    wrote the first version of the logic~LK.  Tobias Nipkow developed
    20    LCF and~Cube.  Martin Coen developed~Modal with assistance
    21    from Rajeev Gor\'e.  The research has been funded by the EPSRC
    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}.} }
    25 
    26 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    27   \hrule\bigskip}
    28 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
    29 
    30 \makeindex
    31 
    32 \underscoreoff
    33 
    34 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    35 
    36 \pagestyle{headings}
    37 \sloppy
    38 \binperiod     %%%treat . like a binary operator
    39 
    40 \begin{document}
    41 \maketitle 
    42 \pagenumbering{roman} \tableofcontents \clearfirst
    43 \include{preface}
    44 \include{syntax}
    45 \include{LK}
    46 \include{Sequents}
    47 %%\include{Modal}
    48 \include{CTT}
    49 \bibliographystyle{plain}
    50 \bibliography{../manual}
    51 \printindex
    52 \end{document}