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