author | wenzelm |
Mon, 27 Aug 2012 22:31:16 +0200 | |
changeset 48950 | 9965099f51ad |
parent 42511 | doc-src/Classes/classes.tex@bf89455ccf9d |
permissions | -rw-r--r-- |
30227 | 1 |
\documentclass[12pt,a4paper,fleqn]{article} |
20946 | 2 |
\usepackage{latexsym,graphicx} |
48950
9965099f51ad
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
3 |
\usepackage{iman,extra,isar,proof} |
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: |