304

1 
%% $ lcp Exp $

285

2 
\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}

358

3 
%\includeonly{Ref/simplifier}

328

4 
%% index{\(\w+\)\!metalevel index{meta\1

285

5 
%%% to index ids: \[\\tt \([azAZ09][azAZ09_'.]*\) [\\ttindexbold{\1}


6 
%% run sedindex springer to prepare index file


7 

304

8 
\sloppy

285

9 


10 
\title{Isabelle\\A Generic Theorem Prover}


11 
\author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}


12 


13 
\date{}


14 
\makeindex

328

15 

285

16 
\def\S{Sect.\thinspace}%This is how Springer like it


17 


18 
\underscoreoff


19 

304

20 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}

285

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

328

32 
\listoffigures


33 
\newpage

285

34 


35 
\markboth{}{}


36 
\newfont{\sanssi}{cmssi12}


37 
\vspace*{2.5cm}

358

38 
\begin{quote}\raggedleft


39 
{\em To Nathan and Sarah}


40 


41 
\vspace*{1.2cm}

285

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 

358

50 
\thispagestyle{empty}


51 
\newpage


52 
\pagenumbering{arabic}


53 
\part{Introduction to Isabelle}

285

54 

328

55 
\index{hypothesessee{assumptions}}


56 
\index{rewritingsee{simplification}}

304

57 
\index{variables!schematicsee{unknowns}}

328

58 
\index{abstract syntax treessee{ASTs}}

285

59 

358

60 
\begingroup%things local to Intro  especially, redefining \part!!

285

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}

328

77 
\include{Ref/defining}


78 
\include{Ref/syntax}

285

79 
\include{Ref/substitution}


80 
\include{Ref/simplifier}


81 
\include{Ref/classical}


82 


83 
\part{Isabelle's ObjectLogics}


84 
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip


85 
\hrule\bigskip}

328

86 
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}


87 

285

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/theorysyntax}


96 


97 
%%seealso's must be last so that they appear last in the index entries

328

98 
\index{backtrackingseealso{{\tt back} command, search}}


99 
\index{classesseealso{sorts}}


100 
\index{sortsseealso{arities}}


101 
\index{axiomsseealso{rules, theorems}}


102 
\index{theoremsseealso{rules}}


103 
\index{definitionsseealso{metarewriting}}


104 
\index{equalityseealso{simplification}}

285

105 


106 
\bibliographystyle{springer} \small\raggedright\frenchspacing


107 
\bibliography{stringabbrv,atp,funprog,general,isabelle,logicprog,theory}


108 


109 
\input{springer.ind}


110 
\end{document}
