author | nipkow |
Fri, 10 Jun 2005 18:36:47 +0200 | |
changeset 16359 | af7239e3054d |
parent 14400 | 6069098854b9 |
child 25257 | 8faf184ba5b1 |
permissions | -rw-r--r-- |
11423 | 1 |
\documentclass{article} |
14400 | 2 |
%%\includeonly{Types/types} %%UNCOMMENT to process only selected chapters |
11423 | 3 |
\usepackage{cl2emono-modified,isabelle,isabellesym} |
4 |
\usepackage{../proof,amsmath,amsfonts} |
|
12639 | 5 |
\usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment} |
13981 | 6 |
\usepackage[greek,english]{babel} |
11423 | 7 |
\usepackage{../pdfsetup} |
8 |
%last package! |
|
9 |
||
10 |
\remarkstrue %TRUE causes remarks to be displayed (as marginal notes) |
|
11 |
%\remarksfalse |
|
12 |
||
13 |
\makeindex |
|
14 |
||
11450 | 15 |
\index{conditional expressions|see{\isa{if} expressions}} |
11456 | 16 |
\index{primitive recursion|see{recursion, primitive}} |
11428 | 17 |
\index{product type|see{pairs and tuples}} |
11456 | 18 |
\index{structural induction|see{induction, structural}} |
11428 | 19 |
\index{termination|see{functions, total}} |
20 |
\index{tuples|see{pairs and tuples}} |
|
11423 | 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} |
|
12790 | 31 |
\title{ |
32 |
\begin{center} |
|
33 |
\includegraphics[scale=.8]{isabelle_hol} |
|
12916 | 34 |
\\ \vspace{0.5cm} A Proof Assistant for Higher-Order Logic |
12790 | 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 |
} |
|
11423 | 42 |
\maketitle |
43 |
||
44 |
\pagenumbering{roman} |
|
45 |
\setcounter{page}{5} |
|
11547 | 46 |
\vspace*{\fill} |
47 |
\begin{center} |
|
11548 | 48 |
\LARGE In memoriam \\[1ex] |
49 |
{\sc Annette Schumann}\\[1ex] |
|
11547 | 50 |
1959 -- 2001 |
51 |
\end{center} |
|
52 |
\vspace*{\fill} |
|
53 |
\vspace*{\fill} |
|
54 |
\newpage |
|
14400 | 55 |
\include{preface} |
11423 | 56 |
|
57 |
\tableofcontents |
|
58 |
||
11450 | 59 |
\cleardoublepage\pagenumbering{arabic} |
11423 | 60 |
|
12669 | 61 |
\part{Elementary Techniques} |
14400 | 62 |
\include{basics} |
63 |
\include{fp} |
|
64 |
\include{Documents/documents} |
|
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
65 |
|
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
66 |
\part{Logic and Sets} |
14400 | 67 |
\include{Rules/rules} |
68 |
\include{Sets/sets} |
|
69 |
\include{Inductive/inductive} |
|
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
70 |
|
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
71 |
\part{Advanced Material} |
14400 | 72 |
\include{Types/types} |
73 |
\include{Advanced/advanced} |
|
74 |
\include{Protocol/protocol} |
|
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
75 |
|
12489 | 76 |
\markboth{}{} |
77 |
\cleardoublepage |
|
78 |
\vspace*{\fill} |
|
79 |
\begin{flushright} |
|
80 |
\begin{tabular}{l} |
|
81 |
{\large\sf\slshape You know my methods. Apply them!}\\[1ex] |
|
82 |
Sherlock Holmes |
|
83 |
\end{tabular} |
|
84 |
\end{flushright} |
|
85 |
\vspace*{\fill} |
|
86 |
\vspace*{\fill} |
|
87 |
||
14400 | 88 |
\underscoreoff |
89 |
||
90 |
\include{appendix} |
|
8743 | 91 |
|
92 |
\bibliographystyle{plain} |
|
93 |
\bibliography{../manual} |
|
14400 | 94 |
\underscoreoff |
8828 | 95 |
\printindex |
8743 | 96 |
\end{document} |