1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Classes/classes.tex	Tue Mar 03 11:00:51 2009 +0100
     1.3 @@ -0,0 +1,50 @@
     1.4 +
     1.5 +\documentclass[12pt,a4paper,fleqn]{report}
     1.6 +\usepackage{latexsym,graphicx}
     1.7 +\usepackage[refpage]{nomencl}
     1.8 +\usepackage{../iman,../extra,../isar,../proof}
     1.9 +\usepackage{../isabelle,../isabellesym}
    1.10 +\usepackage{style}
    1.11 +\usepackage{../pdfsetup}
    1.12 +
    1.13 +
    1.14 +\hyphenation{Isabelle}
    1.15 +\hyphenation{Isar}
    1.16 +\isadroptag{theory}
    1.17 +
    1.18 +\title{\includegraphics[scale=0.5]{isabelle_isar}
    1.19 +  \\[4ex] Haskell-style type classes with Isabelle/Isar}
    1.20 +\author{\emph{Florian Haftmann}}
    1.21 +
    1.22 +\begin{document}
    1.23 +
    1.24 +\maketitle
    1.25 +
    1.26 +\begin{abstract}
    1.27 +  This tutorial introduces the look-and-feel of Isar type classes
    1.28 +  to the end-user; Isar type classes are a convenient mechanism
    1.29 +  for organizing specifications, overcoming some drawbacks
    1.30 +  of raw axiomatic type classes. Essentially, they combine
    1.31 +  an operational aspect (in the manner of Haskell) with
    1.32 +  a logical aspect, both managed uniformly.
    1.33 +\end{abstract}
    1.34 +
    1.35 +\thispagestyle{empty}\clearpage
    1.36 +
    1.37 +\pagenumbering{roman}
    1.38 +\clearfirst
    1.39 +
    1.40 +\input{Thy/document/Classes.tex}
    1.41 +
    1.42 +\begingroup
    1.43 +\bibliographystyle{plain} \small\raggedright\frenchspacing
    1.44 +\bibliography{../manual}
    1.45 +\endgroup
    1.46 +
    1.47 +\end{document}
    1.48 +
    1.49 +
    1.50 +%%% Local Variables: 
    1.51 +%%% mode: latex
    1.52 +%%% TeX-master: t
    1.53 +%%% End: