author | wenzelm |
Sat, 05 Apr 2014 15:03:40 +0200 | |
changeset 56421 | 1ffd7eaa778b |
parent 48985 | 5386df44a037 |
child 62524 | bf9a024ca238 |
permissions | -rw-r--r-- |
11423 | 1 |
\documentclass{article} |
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
2 |
\usepackage{cl2emono-modified,isabelle,isabellesym} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
3 |
\usepackage{proof,amsmath,amsfonts} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
4 |
\usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,ttbox,comment} |
48171
28a6d67c93f0
default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
wenzelm
parents:
42511
diff
changeset
|
5 |
\usepackage{eurosym} |
28a6d67c93f0
default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
wenzelm
parents:
42511
diff
changeset
|
6 |
\usepackage[english]{babel} |
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
7 |
\usepackage{pdfsetup} |
11423 | 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 |
} |
|
30956
9b294296691b
empty page leads to results on duplex printers as expected
haftmann
parents:
26913
diff
changeset
|
42 |
\pagenumbering{roman} |
11423 | 43 |
\maketitle |
30956
9b294296691b
empty page leads to results on duplex printers as expected
haftmann
parents:
26913
diff
changeset
|
44 |
\newpage |
11423 | 45 |
|
30956
9b294296691b
empty page leads to results on duplex printers as expected
haftmann
parents:
26913
diff
changeset
|
46 |
%\setcounter{page}{5} |
25257 | 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 |
|
30956
9b294296691b
empty page leads to results on duplex printers as expected
haftmann
parents:
26913
diff
changeset
|
56 |
|
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
57 |
\input{preface} |
11423 | 58 |
|
59 |
\tableofcontents |
|
60 |
||
11450 | 61 |
\cleardoublepage\pagenumbering{arabic} |
11423 | 62 |
|
12669 | 63 |
\part{Elementary Techniques} |
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
64 |
\input{basics} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
65 |
\input{fp} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
66 |
\input{documents0} |
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
67 |
|
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
68 |
\part{Logic and Sets} |
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
69 |
\input{rules} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
70 |
\input{sets} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
71 |
\input{inductive0} |
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
72 |
|
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
73 |
\part{Advanced Material} |
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
74 |
\input{types0} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
75 |
\input{advanced0} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
76 |
\input{protocol} |
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
77 |
|
12489 | 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 |
||
14400 | 90 |
\underscoreoff |
91 |
||
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
92 |
\input{appendix0} |
8743 | 93 |
|
94 |
\bibliographystyle{plain} |
|
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48525
diff
changeset
|
95 |
\bibliography{manual} |
14400 | 96 |
\underscoreoff |
8828 | 97 |
\printindex |
8743 | 98 |
\end{document} |