doc-src/springer.tex
author lcp
Fri Apr 15 18:34:26 1994 +0200 (1994-04-15)
changeset 328 2d1b460dbb62
parent 304 5edc4f5e5ebd
child 358 df8f0fbf7dbd
permissions -rw-r--r--
penultimate Springer draft
     1 %% $ lcp Exp $
     2 \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
     3 %%\includeonly{Logics/HOL}
     4 %%  index{\(\w+\)\!meta-level     index{meta-\1
     5 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
     6 %% run    sedindex springer    to prepare index file
     7 
     8 \sloppy
     9 
    10 \title{Isabelle\\A Generic Theorem Prover}
    11 \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
    12 
    13 \date{} 
    14 \makeindex
    15 \let\idx=\ttindexbold
    16 %for indexing constants, symbols, theorems, ...
    17 \newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}
    18 \newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}
    19 
    20 \newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}
    21 \newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}
    22 
    23 \newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
    24 \newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}
    25 
    26 \newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
    27 \newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}
    28 
    29 \newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}
    30 \newcommand\tydx[1]{{\tt#1}\index{#1@{\tt#1} type}}
    31 \newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}
    32 
    33 \def\S{Sect.\thinspace}%This is how Springer like it
    34 
    35 \underscoreoff
    36 
    37 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}
    38 
    39 \binperiod     %%%treat . like a binary operator
    40 
    41 \begin{document}
    42 \maketitle
    43 
    44 \pagenumbering{Roman}
    45 \include{preface}
    46 
    47 \tableofcontents
    48 \newpage
    49 \listoffigures
    50 \newpage
    51 
    52 \pagenumbering{arabic}
    53 
    54 \markboth{}{}
    55 \newfont{\sanssi}{cmssi12}
    56 \vspace*{2.5cm}
    57 \begin{quote}
    58 \raggedleft
    59 {\sanssi
    60 You can only find truth with logic\\
    61 if you have already found truth without it.}\\
    62 \bigskip
    63 
    64 G.K. Chesterton, {\em The Man who was Orthodox}
    65 \end{quote}
    66 
    67 
    68 \index{hypotheses|see{assumptions}}
    69 \index{rewriting|see{simplification}}
    70 \index{variables!schematic|see{unknowns}} 
    71 \index{abstract syntax trees|see{ASTs}}
    72 
    73 \part{Introduction to Isabelle}   
    74 
    75 \begingroup
    76 \newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
    77 \newcommand{\nand}{\mathbin{\lnot\&}} 
    78 \newcommand{\xor}{\mathbin{\#}}
    79 \let\part=\chapter
    80 \include{Intro/foundations}
    81 \include{Intro/getting}
    82 \include{Intro/advanced}
    83 \endgroup
    84 
    85 \part{The Isabelle Reference Manual} 
    86 \include{Ref/introduction}
    87 \include{Ref/goals}
    88 \include{Ref/tactic}
    89 \include{Ref/tctical}
    90 \include{Ref/thm}
    91 \include{Ref/theories}
    92 \include{Ref/defining}
    93 \include{Ref/syntax}
    94 \include{Ref/substitution}
    95 \include{Ref/simplifier}
    96 \include{Ref/classical}
    97 
    98 \part{Isabelle's Object-Logics} 
    99 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
   100   \hrule\bigskip}
   101 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
   102 
   103 \include{Logics/intro}
   104 \include{Logics/FOL}
   105 \include{Logics/ZF}
   106 \include{Logics/HOL}
   107 \include{Logics/LK}
   108 \include{Logics/CTT}
   109 
   110 \include{Ref/theory-syntax}
   111 
   112 %%seealso's must be last so that they appear last in the index entries
   113 \index{backtracking|seealso{{\tt back} command, search}}
   114 \index{classes|seealso{sorts}}
   115 \index{sorts|seealso{arities}}
   116 \index{axioms|seealso{rules, theorems}}
   117 \index{theorems|seealso{rules}}
   118 \index{definitions|seealso{meta-rewriting}}
   119 \index{equality|seealso{simplification}}
   120 
   121 \bibliographystyle{springer} \small\raggedright\frenchspacing
   122 \bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
   123 
   124 \input{springer.ind}
   125 \end{document}