doc-src/Logics/logics.tex
author lcp
Wed Nov 10 05:00:57 1993 +0100 (1993-11-10)
changeset 104 d8205bb279a7
child 111 1b3cddf41b2d
permissions -rw-r--r--
Initial revision
lcp@104
     1
\documentstyle[a4,12pt,proof,iman,alltt]{report}
lcp@104
     2
%% $Id$
lcp@104
     3
%%%STILL NEEDS MODAL, LCF
lcp@104
     4
\includeonly{HOL}
lcp@104
     5
%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\idx{\1}  
lcp@104
     6
%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\idx{\1}  
lcp@104
     7
%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\idx{\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@104
    12
\author{{\em Lawrence C. Paulson}\thanks{Tobias Nipkow and Markus Wenzel,
lcp@104
    13
    of T. U. Munich, wrote the chapter `Defining Logics'.  Markus Wenzel
lcp@104
    14
    also suggested changes and corrections.  Philippe de Groote wrote the
lcp@104
    15
    first version of the logic~\LK{} and contributed to~\ZF{}.  Tobias
lcp@104
    16
    Nipkow developed~\HOL{}, \LCF{} and~\Cube{}.  Philippe No\"el and
lcp@104
    17
    Martin Coen made many contributions to~\ZF{}.  Martin Coen
lcp@104
    18
    developed~\Modal{} with assistance from Rajeev Gor\'e.  The research
lcp@104
    19
    has been funded by the SERC (grants GR/G53279, GR/H40570) and by ESPRIT
lcp@104
    20
    project 6453: Types}.\\ 
lcp@104
    21
  Computer Laboratory \\ 
lcp@104
    22
  University of Cambridge \\[2ex] 
lcp@104
    23
  {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} \\[3cm]
lcp@104
    24
  {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson} }
lcp@104
    25
lcp@104
    26
\date{}
lcp@104
    27
lcp@104
    28
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
lcp@104
    29
  \hrule\bigskip}
lcp@104
    30
lcp@104
    31
\makeindex
lcp@104
    32
lcp@104
    33
%For indexing names in ttbox; could be local to Chapters, making a subitem...
lcp@104
    34
\let\idx=\ttindexbold
lcp@104
    35
%%%%\newcommand\idx[1]{\indexbold{*#1}#1}
lcp@104
    36
lcp@104
    37
\underscoreoff
lcp@104
    38
lcp@104
    39
\setcounter{secnumdepth}{1} \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
lcp@104
    48
\include{intro}
lcp@104
    49
\include{FOL}
lcp@104
    50
\include{ZF}
lcp@104
    51
\include{HOL}
lcp@104
    52
\include{LK}
lcp@104
    53
%%\include{Modal}
lcp@104
    54
\include{CTT}
lcp@104
    55
%%\include{Cube}
lcp@104
    56
%%\include{LCF}
lcp@104
    57
\include{defining}
lcp@104
    58
\bibliographystyle{plain}
lcp@104
    59
\bibliography{atp,theory,funprog,logicprog}
lcp@104
    60
\input{logics.ind}
lcp@104
    61
\end{document}