doc-src/springer.tex
author lcp
Mon Mar 21 10:51:28 1994 +0100 (1994-03-21)
changeset 285 fd4a6585e5bf
child 304 5edc4f5e5ebd
permissions -rw-r--r--
first draft of Springer book
     1 \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
     2 %%%\includeonly{preface}
     3 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
     4 %% run    sedindex springer    to prepare index file
     5 
     6 \sloppy%%%????????????????????????????????????????????????????????????????
     7 
     8 \title{Isabelle\\A Generic Theorem Prover}
     9 \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
    10 
    11 \date{} 
    12 \makeindex
    13 \let\idx=\ttindexbold
    14 \def\S{Sect.\thinspace}%This is how Springer like it
    15 
    16 \underscoreoff
    17 
    18 \setcounter{secnumdepth}{1} \setcounter{tocdepth}{1}
    19 
    20 \binperiod     %%%treat . like a binary operator
    21 
    22 \begin{document}
    23 \maketitle
    24 
    25 \pagenumbering{Roman}
    26 \include{preface}
    27 
    28 \tableofcontents
    29 \newpage
    30 
    31 \pagenumbering{arabic}
    32 
    33 \markboth{}{}
    34 \newfont{\sanssi}{cmssi12}
    35 \vspace*{2.5cm}
    36 \begin{quote}
    37 \raggedleft
    38 {\sanssi
    39 You can only find truth with logic\\
    40 if you have already found truth without it.}\\
    41 \bigskip
    42 
    43 G.K. Chesterton, {\em The Man who was Orthodox}
    44 \end{quote}
    45 
    46 
    47 \index{definitions|see{rewriting, meta-level}}
    48 \index{rewriting!object-level|see{simplification}}
    49 \index{rules!meta-level|see{meta-rules}}
    50 \index{scheme variables|see{unknowns}}
    51 \index{AST|see{trees, abstract syntax}}
    52 
    53 \part{Introduction to Isabelle}   
    54 
    55 \begingroup
    56 \newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
    57 \newcommand{\nand}{\mathbin{\lnot\&}} 
    58 \newcommand{\xor}{\mathbin{\#}}
    59 \let\part=\chapter
    60 \include{Intro/foundations}
    61 \include{Intro/getting}
    62 \include{Intro/advanced}
    63 \endgroup
    64 
    65 \part{The Isabelle Reference Manual} 
    66 \include{Ref/introduction}
    67 \include{Ref/goals}
    68 \include{Ref/tactic}
    69 \include{Ref/tctical}
    70 \include{Ref/thm}
    71 \include{Ref/theories}
    72 \include{Ref/substitution}
    73 \include{Ref/simplifier}
    74 \include{Ref/classical}
    75 
    76 \part{Isabelle's Object-Logics} 
    77 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    78   \hrule\bigskip}
    79 \include{Logics/intro}
    80 \include{Logics/FOL}
    81 \include{Logics/ZF}
    82 \include{Logics/HOL}
    83 \include{Logics/LK}
    84 \include{Logics/CTT}
    85 \include{Logics/defining}
    86 
    87 \include{Ref/theory-syntax}
    88 
    89 %%seealso's must be last so that they appear last in the index entries
    90 \index{rewriting!meta-level|seealso{tactics, theorems}}
    91 
    92 \bibliographystyle{springer} \small\raggedright\frenchspacing
    93 \bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
    94 
    95 \input{springer.ind}
    96 \end{document}