author | haftmann |
Thu, 19 Jun 2025 17:15:40 +0200 | |
changeset 82734 | 89347c0cc6a3 |
parent 78682 | 46891e209d72 |
permissions | -rw-r--r-- |
30227 | 1 |
\documentclass[12pt,a4paper,fleqn]{article} |
78682
46891e209d72
proper fontenc for cartouches (amending d052d61da398);
wenzelm
parents:
73723
diff
changeset
|
2 |
\usepackage[T1]{fontenc} |
73401 | 3 |
\usepackage{graphicx} |
50426
d2c60ada3ece
eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005);
wenzelm
parents:
48985
diff
changeset
|
4 |
\usepackage{iman,extra,isar} |
48950
9965099f51ad
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
5 |
\usepackage{isabelle,isabellesym} |
20946 | 6 |
\usepackage{style} |
48950
9965099f51ad
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
7 |
\usepackage{pdfsetup} |
20946 | 8 |
|
9 |
||
10 |
\hyphenation{Isabelle} |
|
11 |
\hyphenation{Isar} |
|
12 |
\isadroptag{theory} |
|
28565 | 13 |
|
73723 | 14 |
\title{\includegraphics[scale=0.5]{isabelle_logo} |
20946 | 15 |
\\[4ex] Haskell-style type classes with Isabelle/Isar} |
16 |
\author{\emph{Florian Haftmann}} |
|
17 |
||
18 |
\begin{document} |
|
19 |
||
20 |
\maketitle |
|
21 |
||
22 |
\begin{abstract} |
|
31691 | 23 |
\noindent This tutorial introduces Isar type classes, which |
31256 | 24 |
are a convenient mechanism for organizing specifications. |
25 |
Essentially, they combine an operational aspect (in the |
|
26 |
manner of Haskell) with a logical aspect, both managed uniformly. |
|
20946 | 27 |
\end{abstract} |
28 |
||
29 |
\thispagestyle{empty}\clearpage |
|
30 |
||
31 |
\pagenumbering{roman} |
|
32 |
\clearfirst |
|
33 |
||
48950
9965099f51ad
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
34 |
\input{Classes.tex} |
20946 | 35 |
|
36 |
\begingroup |
|
37 |
\bibliographystyle{plain} \small\raggedright\frenchspacing |
|
48950
9965099f51ad
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
38 |
\bibliography{manual} |
20946 | 39 |
\endgroup |
40 |
||
41 |
\end{document} |
|
42 |
||
43 |
||
44 |
%%% Local Variables: |
|
45 |
%%% mode: latex |
|
46 |
%%% TeX-master: t |
|
47 |
%%% End: |