doc-src/Logics/logics.tex
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 1226 e9c01f251f5d
child 2661 366190b74832
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 \documentstyle[a4,12pt,proof209,iman,extra,rail]{report}
     2 %% $Id$
     3 %%%STILL NEEDS MODAL, LCF
     4 %%%\includeonly{ZF}
     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{Isabelle's Object-Logics}
    11 
    12 \author{{\em Lawrence C. Paulson}\thanks{Tobias Nipkow and Markus Wenzel
    13     suggested changes and corrections.  Philippe de Groote wrote the
    14     first version of the logic~\LK{} and contributed to~\ZF{}.  Tobias
    15     Nipkow developed~\HOL{}, \LCF{} and~\Cube{}.  Philippe No\"el and
    16     Martin Coen made many contributions to~\ZF{}.  Martin Coen
    17     developed~\Modal{} with assistance from Rajeev Gor\'e.  The research
    18     has been funded by the SERC (grants GR/G53279, GR/H40570) and by ESPRIT
    19     project 6453: Types.}\\ 
    20   Computer Laboratory \\ 
    21   University of Cambridge \\[2ex] 
    22   {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} \\[3cm]
    23   {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson} }
    24 
    25 \date{}
    26 
    27 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    28   \hrule\bigskip}
    29 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
    30 
    31 \makeindex
    32 
    33 %%\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
    34 %%\newtheorem{Example}{Example}[chapter]
    35 
    36 \underscoreoff
    37 
    38 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    39 
    40 \pagestyle{headings}
    41 \sloppy
    42 \binperiod     %%%treat . like a binary operator
    43 
    44 \begin{document}
    45 \maketitle 
    46 \pagenumbering{roman} \tableofcontents \clearfirst
    47 \include{intro}
    48 \include{FOL}
    49 \include{ZF}
    50 \include{HOL}
    51 \include{LK}
    52 %%\include{Modal}
    53 \include{CTT}
    54 %%\include{Cube}
    55 %%\include{LCF}
    56 \bibliographystyle{plain}
    57 \bibliography{string,atp,theory,funprog,logicprog,isabelle,crossref}
    58 \input{logics.ind}
    59 \end{document}