author | wenzelm |
Sat, 05 Jan 2002 01:19:14 +0100 | |
changeset 12639 | 71605f976d50 |
parent 12569 | e290dadee51c |
child 12669 | c1436070c21e |
permissions | -rw-r--r-- |
11423 | 1 |
\documentclass{article} |
2 |
\usepackage{cl2emono-modified,isabelle,isabellesym} |
|
3 |
\usepackage{../proof,amsmath,amsfonts} |
|
12639 | 4 |
\usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment} |
12569 | 5 |
\let\RightarrowOrig=\Rightarrow\usepackage{marvosym}\let\Rightarrow=\RightarrowOrig %bug in marvosym!? |
11423 | 6 |
\usepackage{../pdfsetup} |
7 |
%last package! |
|
8 |
||
9 |
\remarkstrue %TRUE causes remarks to be displayed (as marginal notes) |
|
10 |
%\remarksfalse |
|
11 |
||
12 |
\makeindex |
|
13 |
||
11450 | 14 |
\index{conditional expressions|see{\isa{if} expressions}} |
11456 | 15 |
\index{primitive recursion|see{recursion, primitive}} |
11428 | 16 |
\index{product type|see{pairs and tuples}} |
11456 | 17 |
\index{structural induction|see{induction, structural}} |
11428 | 18 |
\index{termination|see{functions, total}} |
19 |
\index{tuples|see{pairs and tuples}} |
|
20 |
\index{settings|see{flags}} |
|
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} |
|
31 |
\title{\includegraphics[scale=.8]{isabelle_hol} |
|
32 |
\\ \vspace{0.5cm} The Tutorial |
|
33 |
\\ --- DRAFT ---} |
|
11458 | 34 |
\author{Tobias Nipkow and Lawrence C. Paulson\\[1ex] |
11423 | 35 |
Technische Universit{\"a}t M{\"u}nchen \\ |
36 |
Institut f{\"u}r Informatik \\[1ex] |
|
37 |
University of Cambridge\\ |
|
38 |
Computer Laboratory} |
|
39 |
\maketitle |
|
40 |
||
41 |
\pagenumbering{roman} |
|
42 |
\setcounter{page}{5} |
|
11547 | 43 |
\vspace*{\fill} |
44 |
\begin{center} |
|
11548 | 45 |
\LARGE In memoriam \\[1ex] |
46 |
{\sc Annette Schumann}\\[1ex] |
|
11547 | 47 |
1959 -- 2001 |
48 |
\end{center} |
|
49 |
\vspace*{\fill} |
|
50 |
\vspace*{\fill} |
|
51 |
\newpage |
|
11423 | 52 |
\input{preface} |
53 |
||
54 |
\tableofcontents |
|
55 |
||
11450 | 56 |
\cleardoublepage\pagenumbering{arabic} |
11423 | 57 |
|
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
58 |
\part{Basic Techniques} %FIXME rename part to "Basic Concepts" (??) |
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
59 |
\input{basics} %FIXME mmw: rename section, move it before part I (??) |
8743 | 60 |
\input{fp} |
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
61 |
\input{Documents/documents} |
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
62 |
|
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
63 |
\part{Logic and Sets} |
10298 | 64 |
\input{Rules/rules} |
65 |
\input{Sets/sets}\input{CTL/ctl} %these constitute ONE chapter |
|
10212 | 66 |
\input{Inductive/inductive} |
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{Advanced Material} |
10676 | 69 |
\input{Types/types} |
9958 | 70 |
\input{Advanced/advanced} |
11249 | 71 |
\input{Protocol/protocol} |
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11548
diff
changeset
|
72 |
|
12489 | 73 |
\markboth{}{} |
74 |
\cleardoublepage |
|
75 |
\vspace*{\fill} |
|
76 |
\begin{flushright} |
|
77 |
\begin{tabular}{l} |
|
78 |
{\large\sf\slshape You know my methods. Apply them!}\\[1ex] |
|
79 |
Sherlock Holmes |
|
80 |
\end{tabular} |
|
81 |
\end{flushright} |
|
82 |
\vspace*{\fill} |
|
83 |
\vspace*{\fill} |
|
84 |
||
8743 | 85 |
\input{appendix} |
86 |
||
87 |
\bibliographystyle{plain} |
|
88 |
\bibliography{../manual} |
|
8828 | 89 |
\printindex |
8743 | 90 |
\end{document} |