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