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