|
1 \documentclass{article} |
|
2 \usepackage{cl2emono-modified,isabelle,isabellesym} |
|
3 \usepackage{proof,amsmath,amsfonts} |
|
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] |
|
84 Sherlock 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} |