304

1 
%% $ lcp Exp $

285

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

304

3 
%%%\includeonly{Ref/tctical,Ref/thm}

285

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


5 
%% run sedindex springer to prepare index file


6 

304

7 
\sloppy

285

8 


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


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


11 


12 
\date{}


13 
\makeindex


14 
\let\idx=\ttindexbold


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


16 


17 
\underscoreoff


18 

304

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

285

20 


21 
\binperiod %%%treat . like a binary operator


22 


23 
\begin{document}


24 
\maketitle


25 


26 
\pagenumbering{Roman}


27 
\include{preface}


28 


29 
\tableofcontents


30 
\newpage


31 


32 
\pagenumbering{arabic}


33 


34 
\markboth{}{}


35 
\newfont{\sanssi}{cmssi12}


36 
\vspace*{2.5cm}


37 
\begin{quote}


38 
\raggedleft


39 
{\sanssi


40 
You can only find truth with logic\\


41 
if you have already found truth without it.}\\


42 
\bigskip


43 


44 
G.K. Chesterton, {\em The Man who was Orthodox}


45 
\end{quote}


46 


47 

304

48 
\index{type classessee{classes}}

285

49 
\index{definitionssee{rewriting, metalevel}}


50 
\index{rewriting!objectlevelsee{simplification}}


51 
\index{rules!metalevelsee{metarules}}

304

52 
\index{variables!schematicsee{unknowns}}

285

53 
\index{ASTsee{trees, abstract syntax}}


54 


55 
\part{Introduction to Isabelle}


56 


57 
\begingroup


58 
\newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification


59 
\newcommand{\nand}{\mathbin{\lnot\&}}


60 
\newcommand{\xor}{\mathbin{\#}}


61 
\let\part=\chapter


62 
\include{Intro/foundations}


63 
\include{Intro/getting}


64 
\include{Intro/advanced}


65 
\endgroup


66 


67 
\part{The Isabelle Reference Manual}


68 
\include{Ref/introduction}


69 
\include{Ref/goals}


70 
\include{Ref/tactic}


71 
\include{Ref/tctical}


72 
\include{Ref/thm}


73 
\include{Ref/theories}


74 
\include{Ref/substitution}


75 
\include{Ref/simplifier}


76 
\include{Ref/classical}


77 


78 
\part{Isabelle's ObjectLogics}


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


80 
\hrule\bigskip}


81 
\include{Logics/intro}


82 
\include{Logics/FOL}


83 
\include{Logics/ZF}


84 
\include{Logics/HOL}


85 
\include{Logics/LK}


86 
\include{Logics/CTT}


87 
\include{Logics/defining}


88 


89 
\include{Ref/theorysyntax}


90 


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


92 
\index{rewriting!metalevelseealso{tactics, theorems}}


93 


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


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


96 


97 
\input{springer.ind}


98 
\end{document}
