1\documentclass{article} 2\usepackage{cl2emono-modified,isabelle,isabellesym} 3\usepackage{proof,amsmath,amsfonts,amssymb} 4\usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,ttbox,comment} 5\usepackage{eurosym} 6\usepackage[english]{babel} 7\usepackage{pdfsetup} 8%last package! 9 10\remarkstrue %TRUE causes remarks to be displayed (as marginal notes) 11%\remarksfalse 12 13\makeindex 14 15\index{conditional expressions|see{\isa{if} expressions}} 16\index{primitive recursion|see{recursion, primitive}} 17\index{product type|see{pairs and tuples}} 18\index{structural induction|see{induction, structural}} 19\index{termination|see{functions, total}} 20\index{tuples|see{pairs and tuples}} 21\index{*<*lex*>|see{lexicographic product}} 22 23\underscoreoff 24 25\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? 26 27\pagestyle{headings} 28 29 30\begin{document} 31\title{ 32\begin{center} 33\includegraphics[scale=.8]{isabelle_hol} 34 \\ \vspace{0.5cm} A Proof Assistant for Higher-Order Logic 35\end{center}} 36\author{Tobias Nipkow \quad Lawrence C. Paulson \quad Markus Wenzel%\\[1ex] 37%Technische Universit{\"a}t M{\"u}nchen \\ 38%Institut f{\"u}r Informatik \\[1ex] 39%University of Cambridge\\ 40%Computer Laboratory 41} 42\pagenumbering{roman} 43\maketitle 44\newpage 45 46%\setcounter{page}{5} 47%\vspace*{\fill} 48%\begin{center} 49%\LARGE In memoriam \\[1ex] 50%{\sc Annette Schumann}\\[1ex] 51%1959 -- 2001 52%\end{center} 53%\vspace*{\fill} 54%\vspace*{\fill} 55%\newpage 56 57\input{preface} 58 59\tableofcontents 60 61\cleardoublepage\pagenumbering{arabic} 62 63\part{Elementary Techniques} 64\input{basics} 65\input{fp} 66\input{documents0} 67 68\part{Logic and Sets} 69\input{rules} 70\input{sets} 71\input{inductive0} 72 73\part{Advanced Material} 74\input{types0} 75\input{advanced0} 76\input{protocol} 77 78\markboth{}{} 79\cleardoublepage 80\vspace*{\fill} 81\begin{flushright} 82\begin{tabular}{l} 83{\large\sf\slshape You know my methods. Apply them!}\\[1ex] 84Sherlock Holmes 85\end{tabular} 86\end{flushright} 87\vspace*{\fill} 88\vspace*{\fill} 89 90\underscoreoff 91 92\input{appendix0} 93 94\bibliographystyle{plain} 95\bibliography{manual} 96\underscoreoff 97\printindex 98\end{document} 99