doc-src/Logics/logics.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 8979 802acc97fdaf
child 42636 41dff1b862bf
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
paulson@6072
     1
%% $Id$
wenzelm@7837
     2
\documentclass[12pt,a4paper]{report}
wenzelm@9695
     3
\usepackage{graphicx,../iman,../extra,../ttbox,../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
wenzelm@9695
    19
   wrote the first version of the logic~LK.  Tobias Nipkow developed
wenzelm@9695
    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@8979
    22
   (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
paulson@8979
    23
   (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
paulson@8979
    24
  Schwerpunktprogramm \emph{Deduktion}.} }
lcp@104
    25
lcp@104
    26
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
lcp@104
    27
  \hrule\bigskip}
lcp@349
    28
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
lcp@104
    29
lcp@104
    30
\makeindex
lcp@104
    31
lcp@104
    32
\underscoreoff
lcp@104
    33
nipkow@465
    34
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
lcp@104
    35
lcp@104
    36
\pagestyle{headings}
lcp@104
    37
\sloppy
lcp@104
    38
\binperiod     %%%treat . like a binary operator
lcp@104
    39
lcp@104
    40
\begin{document}
lcp@104
    41
\maketitle 
lcp@104
    42
\pagenumbering{roman} \tableofcontents \clearfirst
paulson@6072
    43
\include{preface}
paulson@6072
    44
\include{syntax}
lcp@104
    45
\include{LK}
paulson@7160
    46
\include{Sequents}
lcp@104
    47
%%\include{Modal}
lcp@104
    48
\include{CTT}
lcp@104
    49
\bibliographystyle{plain}
paulson@6592
    50
\bibliography{../manual}
wenzelm@8828
    51
\printindex
lcp@104
    52
\end{document}