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";
wenzelm@7837
     1
\documentclass[12pt,a4paper]{report}
wenzelm@42636
     2
\usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup}
wenzelm@2661
     3
lcp@104
     4
%%%STILL NEEDS MODAL, LCF
lcp@349
     5
%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
lcp@349
     6
%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
lcp@349
     7
%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
lcp@104
     8
%%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
lcp@104
     9
%% run    ../sedindex logics    to prepare index file
wenzelm@6623
    10
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Isabelle's Logics}
lcp@104
    11
paulson@3131
    12
\author{{\em Lawrence C. Paulson}\\
paulson@3131
    13
        Computer Laboratory \\ University of Cambridge \\
paulson@3131
    14
        \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
paulson@3131
    15
        With Contributions by Tobias Nipkow and Markus Wenzel%
paulson@7160
    16
 \thanks{Markus Wenzel made numerous improvements.  Sara Kalvala
paulson@7160
    17
    contributed Chap.\ts\ref{chap:sequents}.  Philippe de Groote
wenzelm@9695
    18
   wrote the first version of the logic~LK.  Tobias Nipkow developed
wenzelm@9695
    19
   LCF and~Cube.  Martin Coen developed~Modal with assistance
paulson@7160
    20
   from Rajeev Gor\'e.  The research has been funded by the EPSRC
paulson@8979
    21
   (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
paulson@8979
    22
   (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
paulson@8979
    23
  Schwerpunktprogramm \emph{Deduktion}.} }
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}