%% $ lcp Exp $
\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
%%\includeonly{Logics/HOL}
%% index{\(\w+\)\!meta-level index{meta-\1
%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1}
%% run sedindex springer to prepare index file
\sloppy
\title{Isabelle\\A Generic Theorem Prover}
\author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
\date{}
\makeindex
\let\idx=\ttindexbold
%for indexing constants, symbols, theorems, ...
\newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}
\newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}
\newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}
\newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}
\newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
\newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}
\newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
\newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}
\newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}
\newcommand\tydx[1]{{\tt#1}\index{#1@{\tt#1} type}}
\newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}
\def\S{Sect.\thinspace}%This is how Springer like it
\underscoreoff
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}
\binperiod %%%treat . like a binary operator
\begin{document}
\maketitle
\pagenumbering{Roman}
\include{preface}
\tableofcontents
\newpage
\listoffigures
\newpage
\pagenumbering{arabic}
\markboth{}{}
\newfont{\sanssi}{cmssi12}
\vspace*{2.5cm}
\begin{quote}
\raggedleft
{\sanssi
You can only find truth with logic\\
if you have already found truth without it.}\\
\bigskip
G.K. Chesterton, {\em The Man who was Orthodox}
\end{quote}
\index{hypotheses|see{assumptions}}
\index{rewriting|see{simplification}}
\index{variables!schematic|see{unknowns}}
\index{abstract syntax trees|see{ASTs}}
\part{Introduction to Isabelle}
\begingroup
\newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification
\newcommand{\nand}{\mathbin{\lnot\&}}
\newcommand{\xor}{\mathbin{\#}}
\let\part=\chapter
\include{Intro/foundations}
\include{Intro/getting}
\include{Intro/advanced}
\endgroup
\part{The Isabelle Reference Manual}
\include{Ref/introduction}
\include{Ref/goals}
\include{Ref/tactic}
\include{Ref/tctical}
\include{Ref/thm}
\include{Ref/theories}
\include{Ref/defining}
\include{Ref/syntax}
\include{Ref/substitution}
\include{Ref/simplifier}
\include{Ref/classical}
\part{Isabelle's Object-Logics}
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
\hrule\bigskip}
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
\include{Logics/intro}
\include{Logics/FOL}
\include{Logics/ZF}
\include{Logics/HOL}
\include{Logics/LK}
\include{Logics/CTT}
\include{Ref/theory-syntax}
%%seealso's must be last so that they appear last in the index entries
\index{backtracking|seealso{{\tt back} command, search}}
\index{classes|seealso{sorts}}
\index{sorts|seealso{arities}}
\index{axioms|seealso{rules, theorems}}
\index{theorems|seealso{rules}}
\index{definitions|seealso{meta-rewriting}}
\index{equality|seealso{simplification}}
\bibliographystyle{springer} \small\raggedright\frenchspacing
\bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
\input{springer.ind}
\end{document}