paulson@11423: \documentclass{article}
paulson@11423: \usepackage{cl2emono-modified,isabelle,isabellesym}
paulson@11423: \usepackage{../proof,amsmath,amsfonts}
wenzelm@12639: \usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment}
wenzelm@12569: \let\RightarrowOrig=\Rightarrow\usepackage{marvosym}\let\Rightarrow=\RightarrowOrig  %bug in marvosym!?
paulson@11423: \usepackage{../pdfsetup}   
paulson@11423: %last package!
paulson@11423: 
paulson@11423: \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
paulson@11423: %\remarksfalse
paulson@11423: 
paulson@11423: \makeindex
paulson@11423: 
paulson@11450: \index{conditional expressions|see{\isa{if} expressions}}
paulson@11456: \index{primitive recursion|see{recursion, primitive}}
paulson@11428: \index{product type|see{pairs and tuples}}
paulson@11456: \index{structural induction|see{induction, structural}}
paulson@11428: \index{termination|see{functions, total}}
paulson@11428: \index{tuples|see{pairs and tuples}}
paulson@11428: \index{settings|see{flags}}
paulson@11423: \index{*<*lex*>|see{lexicographic product}}
paulson@11423: 
paulson@11423: \underscoreoff
paulson@11423: 
paulson@11423: \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
paulson@11423: 
paulson@11423: \pagestyle{headings}
paulson@11423: 
paulson@11423: 
paulson@11423: \begin{document}
nipkow@12790: \title{
nipkow@12790: \begin{center}
nipkow@12790: \includegraphics[scale=.8]{isabelle_hol}
wenzelm@12916:        \\ \vspace{0.5cm} A Proof Assistant for Higher-Order Logic
nipkow@12790: \end{center}}
nipkow@12790: \author{Tobias Nipkow \quad Lawrence C. Paulson \quad Markus Wenzel%\\[1ex]
nipkow@12790: %Technische Universit{\"a}t M{\"u}nchen \\
nipkow@12790: %Institut f{\"u}r Informatik \\[1ex]
nipkow@12790: %University of Cambridge\\
nipkow@12790: %Computer Laboratory
nipkow@12790: }
paulson@11423: \maketitle
paulson@11423: 
paulson@11423: \pagenumbering{roman}
paulson@11423: \setcounter{page}{5}
nipkow@11547: \vspace*{\fill}
nipkow@11547: \begin{center}
nipkow@11548: \LARGE In memoriam \\[1ex]
nipkow@11548: {\sc Annette Schumann}\\[1ex]
nipkow@11547: 1959 -- 2001
nipkow@11547: \end{center}
nipkow@11547: \vspace*{\fill}
nipkow@11547: \vspace*{\fill}
nipkow@11547: \newpage
paulson@11423: \input{preface}
paulson@11423: 
paulson@11423: \tableofcontents
paulson@11423: 
paulson@11450: \cleardoublepage\pagenumbering{arabic}
paulson@11423: 
wenzelm@12669: \part{Elementary Techniques}
wenzelm@12669: \input{basics}
nipkow@8743: \input{fp}
wenzelm@11647: \input{Documents/documents}
wenzelm@11647: 
wenzelm@11647: \part{Logic and Sets}
paulson@10298: \input{Rules/rules}
paulson@10298: \input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
nipkow@10212: \input{Inductive/inductive}
wenzelm@11647: 
wenzelm@11647: \part{Advanced Material}
nipkow@10676: \input{Types/types}
nipkow@9958: \input{Advanced/advanced}
paulson@11249: \input{Protocol/protocol}
wenzelm@11647: 
nipkow@12489: \markboth{}{}
nipkow@12489: \cleardoublepage
nipkow@12489: \vspace*{\fill}
nipkow@12489: \begin{flushright}
nipkow@12489: \begin{tabular}{l}
nipkow@12489: {\large\sf\slshape You know my methods. Apply them!}\\[1ex]
nipkow@12489: Sherlock Holmes
nipkow@12489: \end{tabular}
nipkow@12489: \end{flushright}
nipkow@12489: \vspace*{\fill}
nipkow@12489: \vspace*{\fill}
nipkow@12489: 
nipkow@8743: \input{appendix}
nipkow@8743: 
nipkow@8743: \bibliographystyle{plain}
nipkow@8743: \bibliography{../manual}
wenzelm@8828: \printindex
nipkow@8743: \end{document}