2 \documentclass[12pt,a4paper,fleqn]{article}
3 \usepackage{latexsym,graphicx}
4 \usepackage[refpage]{nomencl}
5 \usepackage{../iman,../extra,../isar,../proof}
6 \usepackage{../isabelle,../isabellesym}
8 \usepackage{../pdfsetup}
11 \hyphenation{Isabelle}
15 \title{\includegraphics[scale=0.5]{isabelle_isar}
16 \\[4ex] Haskell-style type classes with Isabelle/Isar}
17 \author{\emph{Florian Haftmann}}
24 \noindent This tutorial introduces the look-and-feel of
25 Isar type classes to the end-user. Isar type classes
26 are a convenient mechanism for organizing specifications.
27 Essentially, they combine an operational aspect (in the
28 manner of Haskell) with a logical aspect, both managed uniformly.
31 \thispagestyle{empty}\clearpage
36 \input{Thy/document/Classes.tex}
39 \bibliographystyle{plain} \small\raggedright\frenchspacing
40 \bibliography{../manual}