285

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


2 
%%%\includeonly{preface}


3 
%%% to index ids: \[\\tt \([azAZ09][azAZ09_'.]*\) [\\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{definitionssee{rewriting, metalevel}}


48 
\index{rewriting!objectlevelsee{simplification}}


49 
\index{rules!metalevelsee{metarules}}


50 
\index{scheme variablessee{unknowns}}


51 
\index{ASTsee{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 ObjectLogics}


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


88 


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


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


91 


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


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


94 


95 
\input{springer.ind}


96 
\end{document}
