* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.
* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution
%% $ lcp Exp $
\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
%\includeonly{Ref/simplifier}
%% 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
\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
\markboth{}{}
\newfont{\sanssi}{cmssi12}
\vspace*{2.5cm}
\begin{quote}\raggedleft
{\em To Nathan and Sarah}
\vspace*{1.2cm}
{\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}
\thispagestyle{empty}
\newpage
\pagenumbering{arabic}
\part{Introduction to Isabelle}
\index{hypotheses|see{assumptions}}
\index{rewriting|see{simplification}}
\index{variables!schematic|see{unknowns}}
\index{abstract syntax trees|see{ASTs}}
\begingroup%things local to Intro -- especially, redefining \part!!
\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}
\printindex
\end{document}