doc-src/Logics/logics.tex
author wenzelm
Wed Jul 25 12:38:54 2012 +0200 (2012-07-25)
changeset 48497 ba61aceaa18a
parent 42637 381fdcab0f36
permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
     1 \documentclass[12pt,a4paper]{report}
     2 \usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup}
     3 
     4 %%%STILL NEEDS MODAL, LCF
     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}  
     8 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
     9 %% run    ../sedindex logics    to prepare index file
    10 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Isabelle's Logics}
    11 
    12 \author{{\em Lawrence C. Paulson}\\
    13         Computer Laboratory \\ University of Cambridge \\
    14         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
    15         With Contributions by Tobias Nipkow and Markus Wenzel%
    16  \thanks{Markus Wenzel made numerous improvements.  Sara Kalvala
    17     contributed Chap.\ts\ref{chap:sequents}.  Philippe de Groote
    18    wrote the first version of the logic~LK.  Tobias Nipkow developed
    19    LCF and~Cube.  Martin Coen developed~Modal with assistance
    20    from Rajeev Gor\'e.  The research has been funded by the EPSRC
    21    (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
    22    (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
    23   Schwerpunktprogramm \emph{Deduktion}.} }
    24 
    25 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    26   \hrule\bigskip}
    27 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
    28 
    29 \makeindex
    30 
    31 \underscoreoff
    32 
    33 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    34 
    35 \pagestyle{headings}
    36 \sloppy
    37 \binperiod     %%%treat . like a binary operator
    38 
    39 \begin{document}
    40 \maketitle 
    41 \pagenumbering{roman} \tableofcontents \clearfirst
    42 \include{preface}
    43 \include{syntax}
    44 \include{LK}
    45 \include{Sequents}
    46 %%\include{Modal}
    47 \include{CTT}
    48 \bibliographystyle{plain}
    49 \bibliography{../manual}
    50 \printindex
    51 \end{document}