diff -r 2775062fd3a9 -r 2f4684e2ea95 doc-src/Classes/classes.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Classes/classes.tex Tue Mar 03 11:00:51 2009 +0100 @@ -0,0 +1,50 @@ + +\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: