1 \documentclass[11pt,a4paper]{report} |
|
2 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,../pdfsetup} |
|
3 |
|
4 \newcommand\Out[1]{\texttt{\textsl{#1}}} %% for output from terminal sessions |
|
5 |
|
6 %\newtheorem{theorem}{Theorem}[section] |
|
7 \newtheorem{Exercise}{Exercise}[section] |
|
8 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}} |
|
9 \newcommand{\ttlbr}{{\tt[|}} |
|
10 \newcommand{\ttrbr}{{\tt|]}} |
|
11 \newcommand{\ttnot}{\tt\~\relax} |
|
12 \newcommand{\ttor}{\tt|} |
|
13 \newcommand{\ttall}{\tt!} |
|
14 \newcommand{\ttuniquex}{\tt?!} |
|
15 |
|
16 %% $Id$ |
|
17 %%%STILL NEEDS MODAL, LCF |
|
18 %%%\includeonly{ZF} |
|
19 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
|
20 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
|
21 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
|
22 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
|
23 %% run ../sedindex logics to prepare index file |
|
24 |
|
25 \makeindex |
|
26 |
|
27 \underscoreoff |
|
28 |
|
29 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? |
|
30 |
|
31 \pagestyle{headings} |
|
32 %\sloppy |
|
33 %\binperiod %%%treat . like a binary operator |
|
34 |
|
35 \begin{document} |
|
36 \title{\includegraphics[scale=.8]{isabelle_hol} |
|
37 \\ \vspace{0.5cm} The Tutorial |
|
38 \\ --- DRAFT ---} |
|
39 \author{Tobias Nipkow\\ |
|
40 Technische Universit\"at M\"unchen \\ |
|
41 Institut f\"ur Informatik \\ |
|
42 \url{http://www.in.tum.de/~nipkow/}} |
|
43 \maketitle |
|
44 |
|
45 \pagenumbering{roman} |
|
46 \tableofcontents |
|
47 |
|
48 \subsubsection*{Acknowledgements} |
|
49 This tutorial owes a lot to the constant discussions with and the valuable |
|
50 feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller, |
|
51 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch |
|
52 and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to |
|
53 read and comment on a draft version. |
|
54 \clearfirst |
|
55 |
|
56 \input{basics} |
|
57 \input{fp} |
|
58 \input{appendix} |
|
59 |
|
60 \bibliographystyle{plain} |
|
61 \bibliography{../manual} |
|
62 \printindex |
|
63 \end{document} |
|