diff -r f51d4a302962 -r 5386df44a037 src/Doc/Classes/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Classes/document/root.tex Tue Aug 28 18:57:32 2012 +0200 @@ -0,0 +1,46 @@ +\documentclass[12pt,a4paper,fleqn]{article} +\usepackage{latexsym,graphicx} +\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} + \noindent This tutorial introduces Isar type classes, which + are a convenient mechanism for organizing specifications. + 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{Classes.tex} + +\begingroup +\bibliographystyle{plain} \small\raggedright\frenchspacing +\bibliography{manual} +\endgroup + +\end{document} + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: