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
6 \sloppy%%%????????????????????????????????????????????????????????????????
8 \title{Isabelle\\A Generic Theorem Prover}
9 \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
14 \def\S{Sect.\thinspace}%This is how Springer like it
18 \setcounter{secnumdepth}{1} \setcounter{tocdepth}{1}
20 \binperiod %%%treat . like a binary operator
31 \pagenumbering{arabic}
34 \newfont{\sanssi}{cmssi12}
39 You can only find truth with logic\\
40 if you have already found truth without it.}\\
43 G.K. Chesterton, {\em The Man who was Orthodox}
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}}
53 \part{Introduction to Isabelle}
56 \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification
57 \newcommand{\nand}{\mathbin{\lnot\&}}
58 \newcommand{\xor}{\mathbin{\#}}
60 \include{Intro/foundations}
61 \include{Intro/getting}
62 \include{Intro/advanced}
65 \part{The Isabelle Reference Manual}
66 \include{Ref/introduction}
71 \include{Ref/theories}
72 \include{Ref/substitution}
73 \include{Ref/simplifier}
74 \include{Ref/classical}
76 \part{Isabelle's Object-Logics}
77 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
79 \include{Logics/intro}
85 \include{Logics/defining}
87 \include{Ref/theory-syntax}
89 %%seealso's must be last so that they appear last in the index entries
90 \index{rewriting!meta-level|seealso{tactics, theorems}}
92 \bibliographystyle{springer} \small\raggedright\frenchspacing
93 \bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}