1 %% $ lcp Exp $ |
|
2 \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book} |
|
3 %\includeonly{Ref/simplifier} |
|
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 |
|
16 \def\S{Sect.\thinspace}%This is how Springer like it |
|
17 |
|
18 \underscoreoff |
|
19 |
|
20 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{1} |
|
21 |
|
22 \binperiod %%%treat . like a binary operator |
|
23 |
|
24 \begin{document} |
|
25 \maketitle |
|
26 |
|
27 \pagenumbering{Roman} |
|
28 \include{preface} |
|
29 |
|
30 \tableofcontents |
|
31 \newpage |
|
32 \listoffigures |
|
33 \newpage |
|
34 |
|
35 \markboth{}{} |
|
36 \newfont{\sanssi}{cmssi12} |
|
37 \vspace*{2.5cm} |
|
38 \begin{quote}\raggedleft |
|
39 {\em To Nathan and Sarah} |
|
40 |
|
41 \vspace*{1.2cm} |
|
42 {\sanssi |
|
43 You can only find truth with logic\\ |
|
44 if you have already found truth without it.}\\ |
|
45 \bigskip |
|
46 |
|
47 G.K. Chesterton, {\em The Man who was Orthodox} |
|
48 \end{quote} |
|
49 |
|
50 \thispagestyle{empty} |
|
51 \newpage |
|
52 \pagenumbering{arabic} |
|
53 \part{Introduction to Isabelle} |
|
54 |
|
55 \index{hypotheses|see{assumptions}} |
|
56 \index{rewriting|see{simplification}} |
|
57 \index{variables!schematic|see{unknowns}} |
|
58 \index{abstract syntax trees|see{ASTs}} |
|
59 |
|
60 \begingroup%things local to Intro -- especially, redefining \part!! |
|
61 \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification |
|
62 \newcommand{\nand}{\mathbin{\lnot\&}} |
|
63 \newcommand{\xor}{\mathbin{\#}} |
|
64 \let\part=\chapter |
|
65 \include{Intro/foundations} |
|
66 \include{Intro/getting} |
|
67 \include{Intro/advanced} |
|
68 \endgroup |
|
69 |
|
70 \part{The Isabelle Reference Manual} |
|
71 \include{Ref/introduction} |
|
72 \include{Ref/goals} |
|
73 \include{Ref/tactic} |
|
74 \include{Ref/tctical} |
|
75 \include{Ref/thm} |
|
76 \include{Ref/theories} |
|
77 \include{Ref/defining} |
|
78 \include{Ref/syntax} |
|
79 \include{Ref/substitution} |
|
80 \include{Ref/simplifier} |
|
81 \include{Ref/classical} |
|
82 |
|
83 \part{Isabelle's Object-Logics} |
|
84 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
|
85 \hrule\bigskip} |
|
86 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
|
87 |
|
88 \include{Logics/intro} |
|
89 \include{Logics/FOL} |
|
90 \include{Logics/ZF} |
|
91 \include{Logics/HOL} |
|
92 \include{Logics/LK} |
|
93 \include{Logics/CTT} |
|
94 |
|
95 \include{Ref/theory-syntax} |
|
96 |
|
97 %%seealso's must be last so that they appear last in the index entries |
|
98 \index{backtracking|seealso{{\tt back} command, search}} |
|
99 \index{classes|seealso{sorts}} |
|
100 \index{sorts|seealso{arities}} |
|
101 \index{axioms|seealso{rules, theorems}} |
|
102 \index{theorems|seealso{rules}} |
|
103 \index{definitions|seealso{meta-rewriting}} |
|
104 \index{equality|seealso{simplification}} |
|
105 |
|
106 \bibliographystyle{springer} \small\raggedright\frenchspacing |
|
107 \bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory} |
|
108 |
|
109 \printindex |
|
110 \end{document} |
|