lcp@304: %% $ lcp Exp $
lcp@285: \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
lcp@358: %\includeonly{Ref/simplifier}
lcp@328: %%  index{\(\w+\)\!meta-level     index{meta-\1
lcp@285: %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
lcp@285: %% run    sedindex springer    to prepare index file
lcp@285: 
lcp@304: \sloppy
lcp@285: 
lcp@285: \title{Isabelle\\A Generic Theorem Prover}
lcp@285: \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
lcp@285: 
lcp@285: \date{} 
lcp@285: \makeindex
lcp@328: 
lcp@285: \def\S{Sect.\thinspace}%This is how Springer like it
lcp@285: 
lcp@285: \underscoreoff
lcp@285: 
lcp@304: \setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}
lcp@285: 
lcp@285: \binperiod     %%%treat . like a binary operator
lcp@285: 
lcp@285: \begin{document}
lcp@285: \maketitle
lcp@285: 
lcp@285: \pagenumbering{Roman}
lcp@285: \include{preface}
lcp@285: 
lcp@285: \tableofcontents
lcp@285: \newpage
lcp@328: \listoffigures
lcp@328: \newpage
lcp@285: 
lcp@285: \markboth{}{}
lcp@285: \newfont{\sanssi}{cmssi12}
lcp@285: \vspace*{2.5cm}
lcp@358: \begin{quote}\raggedleft
lcp@358: {\em To Nathan and Sarah}
lcp@358: 
lcp@358: \vspace*{1.2cm}
lcp@285: {\sanssi
lcp@285: You can only find truth with logic\\
lcp@285: if you have already found truth without it.}\\
lcp@285: \bigskip
lcp@285: 
lcp@285: G.K. Chesterton, {\em The Man who was Orthodox}
lcp@285: \end{quote}
lcp@285: 
lcp@358: \thispagestyle{empty}
lcp@358: \newpage
lcp@358: \pagenumbering{arabic}
lcp@358: \part{Introduction to Isabelle}   
lcp@285: 
lcp@328: \index{hypotheses|see{assumptions}}
lcp@328: \index{rewriting|see{simplification}}
lcp@304: \index{variables!schematic|see{unknowns}} 
lcp@328: \index{abstract syntax trees|see{ASTs}}
lcp@285: 
lcp@358: \begingroup%things local to Intro -- especially, redefining \part!!
lcp@285: \newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
lcp@285: \newcommand{\nand}{\mathbin{\lnot\&}} 
lcp@285: \newcommand{\xor}{\mathbin{\#}}
lcp@285: \let\part=\chapter
lcp@285: \include{Intro/foundations}
lcp@285: \include{Intro/getting}
lcp@285: \include{Intro/advanced}
lcp@285: \endgroup
lcp@285: 
lcp@285: \part{The Isabelle Reference Manual} 
lcp@285: \include{Ref/introduction}
lcp@285: \include{Ref/goals}
lcp@285: \include{Ref/tactic}
lcp@285: \include{Ref/tctical}
lcp@285: \include{Ref/thm}
lcp@285: \include{Ref/theories}
lcp@328: \include{Ref/defining}
lcp@328: \include{Ref/syntax}
lcp@285: \include{Ref/substitution}
lcp@285: \include{Ref/simplifier}
lcp@285: \include{Ref/classical}
lcp@285: 
lcp@285: \part{Isabelle's Object-Logics} 
lcp@285: \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
lcp@285:   \hrule\bigskip}
lcp@328: \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
lcp@328: 
lcp@285: \include{Logics/intro}
lcp@285: \include{Logics/FOL}
lcp@285: \include{Logics/ZF}
lcp@285: \include{Logics/HOL}
lcp@285: \include{Logics/LK}
lcp@285: \include{Logics/CTT}
lcp@285: 
lcp@285: \include{Ref/theory-syntax}
lcp@285: 
lcp@285: %%seealso's must be last so that they appear last in the index entries
lcp@328: \index{backtracking|seealso{{\tt back} command, search}}
lcp@328: \index{classes|seealso{sorts}}
lcp@328: \index{sorts|seealso{arities}}
lcp@328: \index{axioms|seealso{rules, theorems}}
lcp@328: \index{theorems|seealso{rules}}
lcp@328: \index{definitions|seealso{meta-rewriting}}
lcp@328: \index{equality|seealso{simplification}}
lcp@285: 
lcp@285: \bibliographystyle{springer} \small\raggedright\frenchspacing
lcp@285: \bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
lcp@285: 
wenzelm@8828: \printindex
lcp@285: \end{document}