| author | blanchet | 
| Fri, 01 Aug 2014 14:43:57 +0200 | |
| changeset 57753 | 643e02500991 | 
| parent 50426 | d2c60ada3ece | 
| child 73401 | 8b464825d2b5 | 
| permissions | -rw-r--r-- | 
| 30227 | 1  | 
\documentclass[12pt,a4paper,fleqn]{article}
 | 
| 20946 | 2  | 
\usepackage{latexsym,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
 | 
3  | 
\usepackage{iman,extra,isar}
 | 
| 
48950
 
9965099f51ad
more standard document preparation within session context;
 
wenzelm 
parents: 
42511 
diff
changeset
 | 
4  | 
\usepackage{isabelle,isabellesym}
 | 
| 20946 | 5  | 
\usepackage{style}
 | 
| 
48950
 
9965099f51ad
more standard document preparation within session context;
 
wenzelm 
parents: 
42511 
diff
changeset
 | 
6  | 
\usepackage{pdfsetup}
 | 
| 20946 | 7  | 
|
8  | 
||
9  | 
\hyphenation{Isabelle}
 | 
|
10  | 
\hyphenation{Isar}
 | 
|
11  | 
\isadroptag{theory}
 | 
|
| 28565 | 12  | 
|
| 20946 | 13  | 
\title{\includegraphics[scale=0.5]{isabelle_isar}
 | 
14  | 
\\[4ex] Haskell-style type classes with Isabelle/Isar}  | 
|
15  | 
\author{\emph{Florian Haftmann}}
 | 
|
16  | 
||
17  | 
\begin{document}
 | 
|
18  | 
||
19  | 
\maketitle  | 
|
20  | 
||
21  | 
\begin{abstract}
 | 
|
| 31691 | 22  | 
\noindent This tutorial introduces Isar type classes, which  | 
| 31256 | 23  | 
are a convenient mechanism for organizing specifications.  | 
24  | 
Essentially, they combine an operational aspect (in the  | 
|
25  | 
manner of Haskell) with a logical aspect, both managed uniformly.  | 
|
| 20946 | 26  | 
\end{abstract}
 | 
27  | 
||
28  | 
\thispagestyle{empty}\clearpage
 | 
|
29  | 
||
30  | 
\pagenumbering{roman}
 | 
|
31  | 
\clearfirst  | 
|
32  | 
||
| 
48950
 
9965099f51ad
more standard document preparation within session context;
 
wenzelm 
parents: 
42511 
diff
changeset
 | 
33  | 
\input{Classes.tex}
 | 
| 20946 | 34  | 
|
35  | 
\begingroup  | 
|
36  | 
\bibliographystyle{plain} \small\raggedright\frenchspacing
 | 
|
| 
48950
 
9965099f51ad
more standard document preparation within session context;
 
wenzelm 
parents: 
42511 
diff
changeset
 | 
37  | 
\bibliography{manual}
 | 
| 20946 | 38  | 
\endgroup  | 
39  | 
||
40  | 
\end{document}
 | 
|
41  | 
||
42  | 
||
43  | 
%%% Local Variables:  | 
|
44  | 
%%% mode: latex  | 
|
45  | 
%%% TeX-master: t  | 
|
46  | 
%%% End:  |