equal
deleted
inserted
replaced
1 |
|
2 \documentclass[12pt,a4paper,fleqn]{report} |
|
3 \usepackage{graphicx,../iman,../extra,../isar} |
|
4 \usepackage{generated/isabelle,generated/isabellesym} |
|
5 \usepackage{../pdfsetup} % last one! |
|
6 |
|
7 \isabellestyle{it} |
|
8 |
|
9 \renewcommand{\isacommand}[1] |
|
10 {\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof} |
|
11 {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}} |
|
12 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}} |
|
13 \newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}} |
|
14 \newcommand{\dummyproof}{$\DUMMYPROOF$} |
|
15 |
|
16 \newcommand{\cmd}[1]{\isacommand{#1}} |
|
17 |
|
18 \newcommand{\secref}[1]{\S\ref{#1}} |
|
19 \newcommand{\figref}[1]{figure~\ref{#1}} |
|
20 |
|
21 \hyphenation{Isabelle} |
|
22 \hyphenation{Isar} |
|
23 \hyphenation{Haskell} |
|
24 |
|
25 \title{\includegraphics[scale=0.5]{isabelle_isar} |
|
26 \\[4ex] The Art of structured proof composition \\ in Isabelle/Isar} |
|
27 \author{\emph{Markus Wenzel} \\ TU M\"unchen} |
|
28 |
|
29 |
|
30 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} |
|
31 |
|
32 \pagestyle{headings} |
|
33 \sloppy |
|
34 \binperiod %%%treat . like a binary operator |
|
35 |
|
36 |
|
37 \begin{document} |
|
38 |
|
39 \underscoreoff |
|
40 |
|
41 \maketitle |
|
42 |
|
43 \begin{abstract} |
|
44 FIXME |
|
45 \end{abstract} |
|
46 |
|
47 |
|
48 \pagenumbering{roman} \tableofcontents \clearfirst |
|
49 |
|
50 \input{generated/Tutorial} |
|
51 |
|
52 \begingroup |
|
53 \bibliographystyle{plain} \small\raggedright\frenchspacing |
|
54 \bibliography{../manual} |
|
55 \endgroup |
|
56 |
|
57 \nocite{Wenzel-PhD} |
|
58 |
|
59 \end{document} |
|
60 |
|
61 %%% Local Variables: |
|
62 %%% mode: latex |
|
63 %%% TeX-master: t |
|
64 %%% End: |
|