author | kleing |
Sat, 30 Apr 2005 14:18:36 +0200 | |
changeset 15900 | d6156cb8dc2e |
parent 14400 | 6069098854b9 |
child 16359 | af7239e3054d |
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}} |
|
21 |
\index{settings|see{flags}} |
|
11423 | 22 |
\index{*<*lex*>|see{lexicographic product}} |
23 |
||
24 |
\underscoreoff |
|
25 |
||
26 |
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? |
|
27 |
||
28 |
\pagestyle{headings} |
|
29 |
||
30 |
||
31 |
\begin{document} |
|
12790 | 32 |
\title{ |
33 |
\begin{center} |
|
34 |
\includegraphics[scale=.8]{isabelle_hol} |
|
12916 | 35 |
\\ \vspace{0.5cm} A Proof Assistant for Higher-Order Logic |
12790 | 36 |
\end{center}} |
37 |
\author{Tobias Nipkow \quad Lawrence C. Paulson \quad Markus Wenzel%\\[1ex] |
|
38 |
%Technische Universit{\"a}t M{\"u}nchen \\ |
|
39 |
%Institut f{\"u}r Informatik \\[1ex] |
|
40 |
%University of Cambridge\\ |
|
41 |
%Computer Laboratory |
|
42 |
} |
|
11423 | 43 |
\maketitle |
44 |
||
45 |
\pagenumbering{roman} |
|
46 |
\setcounter{page}{5} |
|
11547 | 47 |
\vspace*{\fill} |
48 |
\begin{center} |
|
11548 | 49 |
\LARGE In memoriam \\[1ex] |
50 |
{\sc Annette Schumann}\\[1ex] |
|
11547 | 51 |
1959 -- 2001 |
52 |
\end{center} |
|
53 |
\vspace*{\fill} |
|
54 |
\vspace*{\fill} |
|
55 |
\newpage |
|
14400 | 56 |
\include{preface} |
11423 | 57 |
|
58 |
\tableofcontents |
|
59 |
||
11450 | 60 |
\cleardoublepage\pagenumbering{arabic} |
11423 | 61 |
|
12669 | 62 |
\part{Elementary Techniques} |
14400 | 63 |
\include{basics} |
64 |
\include{fp} |
|
65 |
\include{Documents/documents} |
|
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
66 |
|
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
67 |
\part{Logic and Sets} |
14400 | 68 |
\include{Rules/rules} |
69 |
\include{Sets/sets} |
|
70 |
\include{Inductive/inductive} |
|
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
71 |
|
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
72 |
\part{Advanced Material} |
14400 | 73 |
\include{Types/types} |
74 |
\include{Advanced/advanced} |
|
75 |
\include{Protocol/protocol} |
|
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
76 |
|
12489 | 77 |
\markboth{}{} |
78 |
\cleardoublepage |
|
79 |
\vspace*{\fill} |
|
80 |
\begin{flushright} |
|
81 |
\begin{tabular}{l} |
|
82 |
{\large\sf\slshape You know my methods. Apply them!}\\[1ex] |
|
83 |
Sherlock Holmes |
|
84 |
\end{tabular} |
|
85 |
\end{flushright} |
|
86 |
\vspace*{\fill} |
|
87 |
\vspace*{\fill} |
|
88 |
||
14400 | 89 |
\underscoreoff |
90 |
||
91 |
\include{appendix} |
|
8743 | 92 |
|
93 |
\bibliographystyle{plain} |
|
94 |
\bibliography{../manual} |
|
14400 | 95 |
\underscoreoff |
8828 | 96 |
\printindex |
8743 | 97 |
\end{document} |