wneuper/isa: doc-src/Classes/classes.tex@20e3616b2d9c

     2 \documentclass[12pt,a4paper,fleqn]{article}

     3 \usepackage{latexsym,graphicx}

     4 \usepackage[refpage]{nomencl}

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

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

     7 \usepackage{style}

     8 \usepackage{../pdfsetup}

    11 \hyphenation{Isabelle}

    12 \hyphenation{Isar}

    13 \isadroptag{theory}

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

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

    17 \author{\emph{Florian Haftmann}}

    19 \begin{document}

    21 \maketitle

    23 \begin{abstract}

    24   \noindent This tutorial introduces Isar type classes, which

    25   are a convenient mechanism for organizing specifications.

    26   Essentially, they combine an operational aspect (in the

    27   manner of Haskell) with a logical aspect, both managed uniformly.

    28 \end{abstract}

    30 \thispagestyle{empty}\clearpage

    32 \pagenumbering{roman}

    33 \clearfirst

    35 \input{Thy/document/Classes.tex}

    37 \begingroup

    38 \bibliographystyle{plain} \small\raggedright\frenchspacing

    39 \bibliography{../manual}

    40 \endgroup

    42 \end{document}

    45 %%% Local Variables:

    46 %%% mode: latex

    47 %%% TeX-master: t

    48 %%% End:

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 31684	7d50527dc008
child 43382	bf89455ccf9d
permissions	-rw-r--r--