1\documentclass[12pt,a4paper,fleqn]{article} 2\usepackage{latexsym,graphicx} 3\usepackage{iman,extra,isar} 4\usepackage{isabelle,isabellesym} 5\usepackage{style} 6\usepackage{pdfsetup} 7 8 9\hyphenation{Isabelle} 10\hyphenation{Isar} 11\isadroptag{theory} 12 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} 22 \noindent This tutorial introduces Isar type classes, which 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. 26\end{abstract} 27 28\thispagestyle{empty}\clearpage 29 30\pagenumbering{roman} 31\clearfirst 32 33\input{Classes.tex} 34 35\begingroup 36\bibliographystyle{plain} \small\raggedright\frenchspacing 37\bibliography{manual} 38\endgroup 39 40\end{document} 41 42 43%%% Local Variables: 44%%% mode: latex 45%%% TeX-master: t 46%%% End: 47