\documentclass[12pt,a4paper,fleqn]{report}

 \usepackage{latexsym,graphicx}

 \usepackage[refpage]{nomencl}

 \usepackage{../../iman,../../extra,../../isar,../../proof}

 \usepackage{../../isabelle,../../isabellesym}

 \usepackage{style}

 \usepackage{../../pdfsetup}

 \hyphenation{Isabelle}

 \hyphenation{Isar}

 \isadroptag{theory}

 \title{\includegraphics[scale=0.5]{isabelle_isar}

   \\[4ex] Haskell-style type classes with Isabelle/Isar}

 \author{\emph{Florian Haftmann}}

 \begin{document}

 \maketitle

 \begin{abstract}

   This tutorial introduces the look-and-feel of Isar type classes

   to the end-user; Isar type classes are a convenient mechanism

   for organizing specifications, overcoming some drawbacks

   of raw axiomatic type classes. Essentially, they combine

   an operational aspect (in the manner of Haskell) with

   a logical aspect, both managed uniformly.

 \end{abstract}

 \thispagestyle{empty}\clearpage

 \pagenumbering{roman}

 \clearfirst

 \input{Thy/document/Classes.tex}

 \begingroup

 \bibliographystyle{plain} \small\raggedright\frenchspacing

 \bibliography{../../manual}

 \endgroup

 \end{document}

 %%% Local Variables: 

 %%% mode: latex

 %%% TeX-master: t

 %%% End: