equal
deleted
inserted
replaced
|
1 |
|
2 \documentclass[12pt,a4paper,fleqn]{report} |
|
3 \usepackage{latexsym,graphicx} |
|
4 \usepackage[refpage]{nomencl} |
|
5 \usepackage{../iman,../extra,../isar,../proof} |
|
6 \usepackage{../isabelle,../isabellesym} |
|
7 \usepackage{style} |
|
8 \usepackage{../pdfsetup} |
|
9 |
|
10 |
|
11 \hyphenation{Isabelle} |
|
12 \hyphenation{Isar} |
|
13 \isadroptag{theory} |
|
14 |
|
15 \title{\includegraphics[scale=0.5]{isabelle_isar} |
|
16 \\[4ex] Haskell-style type classes with Isabelle/Isar} |
|
17 \author{\emph{Florian Haftmann}} |
|
18 |
|
19 \begin{document} |
|
20 |
|
21 \maketitle |
|
22 |
|
23 \begin{abstract} |
|
24 This tutorial introduces the look-and-feel of Isar type classes |
|
25 to the end-user; Isar type classes are a convenient mechanism |
|
26 for organizing specifications, overcoming some drawbacks |
|
27 of raw axiomatic type classes. Essentially, they combine |
|
28 an operational aspect (in the manner of Haskell) with |
|
29 a logical aspect, both managed uniformly. |
|
30 \end{abstract} |
|
31 |
|
32 \thispagestyle{empty}\clearpage |
|
33 |
|
34 \pagenumbering{roman} |
|
35 \clearfirst |
|
36 |
|
37 \input{Thy/document/Classes.tex} |
|
38 |
|
39 \begingroup |
|
40 \bibliographystyle{plain} \small\raggedright\frenchspacing |
|
41 \bibliography{../manual} |
|
42 \endgroup |
|
43 |
|
44 \end{document} |
|
45 |
|
46 |
|
47 %%% Local Variables: |
|
48 %%% mode: latex |
|
49 %%% TeX-master: t |
|
50 %%% End: |