1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/springer.tex	Mon Mar 21 10:51:28 1994 +0100
     1.3 @@ -0,0 +1,96 @@
     1.4 +\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
     1.5 +%%%\includeonly{preface}
     1.6 +%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
     1.7 +%% run    sedindex springer    to prepare index file
     1.8 +
     1.9 +\sloppy%%%????????????????????????????????????????????????????????????????
    1.10 +
    1.11 +\title{Isabelle\\A Generic Theorem Prover}
    1.12 +\author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
    1.13 +
    1.14 +\date{} 
    1.15 +\makeindex
    1.16 +\let\idx=\ttindexbold
    1.17 +\def\S{Sect.\thinspace}%This is how Springer like it
    1.18 +
    1.19 +\underscoreoff
    1.20 +
    1.21 +\setcounter{secnumdepth}{1} \setcounter{tocdepth}{1}
    1.22 +
    1.23 +\binperiod     %%%treat . like a binary operator
    1.24 +
    1.25 +\begin{document}
    1.26 +\maketitle
    1.27 +
    1.28 +\pagenumbering{Roman}
    1.29 +\include{preface}
    1.30 +
    1.31 +\tableofcontents
    1.32 +\newpage
    1.33 +
    1.34 +\pagenumbering{arabic}
    1.35 +
    1.36 +\markboth{}{}
    1.37 +\newfont{\sanssi}{cmssi12}
    1.38 +\vspace*{2.5cm}
    1.39 +\begin{quote}
    1.40 +\raggedleft
    1.41 +{\sanssi
    1.42 +You can only find truth with logic\\
    1.43 +if you have already found truth without it.}\\
    1.44 +\bigskip
    1.45 +
    1.46 +G.K. Chesterton, {\em The Man who was Orthodox}
    1.47 +\end{quote}
    1.48 +
    1.49 +
    1.50 +\index{definitions|see{rewriting, meta-level}}
    1.51 +\index{rewriting!object-level|see{simplification}}
    1.52 +\index{rules!meta-level|see{meta-rules}}
    1.53 +\index{scheme variables|see{unknowns}}
    1.54 +\index{AST|see{trees, abstract syntax}}
    1.55 +
    1.56 +\part{Introduction to Isabelle}   
    1.57 +
    1.58 +\begingroup
    1.59 +\newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
    1.60 +\newcommand{\nand}{\mathbin{\lnot\&}} 
    1.61 +\newcommand{\xor}{\mathbin{\#}}
    1.62 +\let\part=\chapter
    1.63 +\include{Intro/foundations}
    1.64 +\include{Intro/getting}
    1.65 +\include{Intro/advanced}
    1.66 +\endgroup
    1.67 +
    1.68 +\part{The Isabelle Reference Manual} 
    1.69 +\include{Ref/introduction}
    1.70 +\include{Ref/goals}
    1.71 +\include{Ref/tactic}
    1.72 +\include{Ref/tctical}
    1.73 +\include{Ref/thm}
    1.74 +\include{Ref/theories}
    1.75 +\include{Ref/substitution}
    1.76 +\include{Ref/simplifier}
    1.77 +\include{Ref/classical}
    1.78 +
    1.79 +\part{Isabelle's Object-Logics} 
    1.80 +\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    1.81 +  \hrule\bigskip}
    1.82 +\include{Logics/intro}
    1.83 +\include{Logics/FOL}
    1.84 +\include{Logics/ZF}
    1.85 +\include{Logics/HOL}
    1.86 +\include{Logics/LK}
    1.87 +\include{Logics/CTT}
    1.88 +\include{Logics/defining}
    1.89 +
    1.90 +\include{Ref/theory-syntax}
    1.91 +
    1.92 +%%seealso's must be last so that they appear last in the index entries
    1.93 +\index{rewriting!meta-level|seealso{tactics, theorems}}
    1.94 +
    1.95 +\bibliographystyle{springer} \small\raggedright\frenchspacing
    1.96 +\bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
    1.97 +
    1.98 +\input{springer.ind}
    1.99 +\end{document}