|
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 |
|
5 |
|
6 \sloppy%%%???????????????????????????????????????????????????????????????? |
|
7 |
|
8 \title{Isabelle\\A Generic Theorem Prover} |
|
9 \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow} |
|
10 |
|
11 \date{} |
|
12 \makeindex |
|
13 \let\idx=\ttindexbold |
|
14 \def\S{Sect.\thinspace}%This is how Springer like it |
|
15 |
|
16 \underscoreoff |
|
17 |
|
18 \setcounter{secnumdepth}{1} \setcounter{tocdepth}{1} |
|
19 |
|
20 \binperiod %%%treat . like a binary operator |
|
21 |
|
22 \begin{document} |
|
23 \maketitle |
|
24 |
|
25 \pagenumbering{Roman} |
|
26 \include{preface} |
|
27 |
|
28 \tableofcontents |
|
29 \newpage |
|
30 |
|
31 \pagenumbering{arabic} |
|
32 |
|
33 \markboth{}{} |
|
34 \newfont{\sanssi}{cmssi12} |
|
35 \vspace*{2.5cm} |
|
36 \begin{quote} |
|
37 \raggedleft |
|
38 {\sanssi |
|
39 You can only find truth with logic\\ |
|
40 if you have already found truth without it.}\\ |
|
41 \bigskip |
|
42 |
|
43 G.K. Chesterton, {\em The Man who was Orthodox} |
|
44 \end{quote} |
|
45 |
|
46 |
|
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}} |
|
52 |
|
53 \part{Introduction to Isabelle} |
|
54 |
|
55 \begingroup |
|
56 \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification |
|
57 \newcommand{\nand}{\mathbin{\lnot\&}} |
|
58 \newcommand{\xor}{\mathbin{\#}} |
|
59 \let\part=\chapter |
|
60 \include{Intro/foundations} |
|
61 \include{Intro/getting} |
|
62 \include{Intro/advanced} |
|
63 \endgroup |
|
64 |
|
65 \part{The Isabelle Reference Manual} |
|
66 \include{Ref/introduction} |
|
67 \include{Ref/goals} |
|
68 \include{Ref/tactic} |
|
69 \include{Ref/tctical} |
|
70 \include{Ref/thm} |
|
71 \include{Ref/theories} |
|
72 \include{Ref/substitution} |
|
73 \include{Ref/simplifier} |
|
74 \include{Ref/classical} |
|
75 |
|
76 \part{Isabelle's Object-Logics} |
|
77 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
|
78 \hrule\bigskip} |
|
79 \include{Logics/intro} |
|
80 \include{Logics/FOL} |
|
81 \include{Logics/ZF} |
|
82 \include{Logics/HOL} |
|
83 \include{Logics/LK} |
|
84 \include{Logics/CTT} |
|
85 \include{Logics/defining} |
|
86 |
|
87 \include{Ref/theory-syntax} |
|
88 |
|
89 %%seealso's must be last so that they appear last in the index entries |
|
90 \index{rewriting!meta-level|seealso{tactics, theorems}} |
|
91 |
|
92 \bibliographystyle{springer} \small\raggedright\frenchspacing |
|
93 \bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory} |
|
94 |
|
95 \input{springer.ind} |
|
96 \end{document} |