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