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
10 \title{Isabelle\\A Generic Theorem Prover}
11 \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
16 \def\S{Sect.\thinspace}%This is how Springer like it
20 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}
22 \binperiod %%%treat . like a binary operator
36 \newfont{\sanssi}{cmssi12}
38 \begin{quote}\raggedleft
39 {\em To Nathan and Sarah}
43 You can only find truth with logic\\
44 if you have already found truth without it.}\\
47 G.K. Chesterton, {\em The Man who was Orthodox}
52 \pagenumbering{arabic}
53 \part{Introduction to Isabelle}
55 \index{hypotheses|see{assumptions}}
56 \index{rewriting|see{simplification}}
57 \index{variables!schematic|see{unknowns}}
58 \index{abstract syntax trees|see{ASTs}}
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{\#}}
65 \include{Intro/foundations}
66 \include{Intro/getting}
67 \include{Intro/advanced}
70 \part{The Isabelle Reference Manual}
71 \include{Ref/introduction}
76 \include{Ref/theories}
77 \include{Ref/defining}
79 \include{Ref/substitution}
80 \include{Ref/simplifier}
81 \include{Ref/classical}
83 \part{Isabelle's Object-Logics}
84 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
86 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
88 \include{Logics/intro}
95 \include{Ref/theory-syntax}
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}}
106 \bibliographystyle{springer} \small\raggedright\frenchspacing
107 \bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}