doc-src/Logics/logics.tex
changeset 349 0ddc495e8b83
parent 317 8a96a64e0b35
child 463 afb7259aebb8
equal deleted inserted replaced
348:1f5a94209c97 349:0ddc495e8b83
     1 \documentstyle[a4,12pt,proof,iman,extra]{report}
     1 \documentstyle[a4,12pt,proof,iman,extra]{report}
     2 %% $Id$
     2 %% $Id$
     3 %%%STILL NEEDS MODAL, LCF
     3 %%%STILL NEEDS MODAL, LCF
     4 %%%\includeonly{ZF}
     4 %%%\includeonly{ZF}
     5 %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\idx{\1}  
     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_]*\),     \\idx{\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_]*\)     \\idx{\1}  
     7 %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
     8 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
     8 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
     9 %% run    ../sedindex logics    to prepare index file
     9 %% run    ../sedindex logics    to prepare index file
    10 \title{Isabelle's Object-Logics}
    10 \title{Isabelle's Object-Logics}
    11 
    11 
    12 \author{{\em Lawrence C. Paulson}\thanks{Tobias Nipkow and Markus Wenzel
    12 \author{{\em Lawrence C. Paulson}\thanks{Tobias Nipkow and Markus Wenzel
    14     first version of the logic~\LK{} and contributed to~\ZF{}.  Tobias
    14     first version of the logic~\LK{} and contributed to~\ZF{}.  Tobias
    15     Nipkow developed~\HOL{}, \LCF{} and~\Cube{}.  Philippe No\"el and
    15     Nipkow developed~\HOL{}, \LCF{} and~\Cube{}.  Philippe No\"el and
    16     Martin Coen made many contributions to~\ZF{}.  Martin Coen
    16     Martin Coen made many contributions to~\ZF{}.  Martin Coen
    17     developed~\Modal{} with assistance from Rajeev Gor\'e.  The research
    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
    18     has been funded by the SERC (grants GR/G53279, GR/H40570) and by ESPRIT
    19     project 6453: Types}.\\ 
    19     project 6453: Types.}\\ 
    20   Computer Laboratory \\ 
    20   Computer Laboratory \\ 
    21   University of Cambridge \\[2ex] 
    21   University of Cambridge \\[2ex] 
    22   {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} \\[3cm]
    22   {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} \\[3cm]
    23   {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson} }
    23   {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson} }
    24 
    24 
    25 \date{}
    25 \date{}
    26 
    26 
    27 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    27 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    28   \hrule\bigskip}
    28   \hrule\bigskip}
       
    29 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
    29 
    30 
    30 \makeindex
    31 \makeindex
    31 
       
    32 %For indexing names in ttbox; could be local to Chapters, making a subitem...
       
    33 \let\idx=\ttindexbold
       
    34 %%%%\newcommand\idx[1]{\indexbold{*#1}#1}
       
    35 
    32 
    36 %%\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
    33 %%\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
    37 %%\newtheorem{Example}{Example}[chapter]
    34 %%\newtheorem{Example}{Example}[chapter]
    38 
    35 
    39 \underscoreoff
    36 \underscoreoff
    55 %%\include{Modal}
    52 %%\include{Modal}
    56 \include{CTT}
    53 \include{CTT}
    57 %%\include{Cube}
    54 %%\include{Cube}
    58 %%\include{LCF}
    55 %%\include{LCF}
    59 \bibliographystyle{plain}
    56 \bibliographystyle{plain}
    60 \bibliography{atp,theory,funprog,logicprog,isabelle}
    57 \bibliography{string,atp,theory,funprog,logicprog,isabelle}
    61 \input{logics.ind}
    58 \input{logics.ind}
    62 \end{document}
    59 \end{document}