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