haftmann@20946: 
haftmann@20946: %% $Id$
haftmann@20946: 
haftmann@20946: \documentclass[12pt,a4paper,fleqn]{report}
haftmann@20946: \usepackage{latexsym,graphicx}
haftmann@20946: \usepackage[refpage]{nomencl}
haftmann@20946: \usepackage{../../iman,../../extra,../../isar,../../proof}
wenzelm@26911: \usepackage{../../isabelle,../../isabellesym}
haftmann@20946: \usepackage{style}
wenzelm@26911: \usepackage{../../pdfsetup}
haftmann@20946: 
haftmann@28540: 
haftmann@28565: %% setup
haftmann@28540: 
haftmann@28565: % hyphenation
haftmann@20946: \hyphenation{Isabelle}
haftmann@20946: \hyphenation{Isar}
haftmann@20946: 
haftmann@28565: % logical markup
haftmann@28565: \newcommand{\strong}[1]{{\bfseries {#1}}}
haftmann@28565: \newcommand{\qn}[1]{\emph{#1}}
haftmann@28565: 
haftmann@28565: % typographic conventions
haftmann@28565: \newcommand{\qt}[1]{``{#1}''}
haftmann@28565: 
haftmann@28565: % verbatim text
haftmann@28565: \newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
haftmann@28565: 
haftmann@28565: % invisibility
haftmann@20946: \isadroptag{theory}
haftmann@28565: 
haftmann@28565: % quoted segments
haftmann@28565: \makeatletter
haftmann@28565: \isakeeptag{quote}
haftmann@28565: \newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
haftmann@28565: \renewcommand{\isatagquote}{\begin{quotesegment}}
haftmann@28565: \renewcommand{\endisatagquote}{\end{quotesegment}}
haftmann@28565: \makeatother
haftmann@28565: 
haftmann@28565: %\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
haftmann@28565: %\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
haftmann@28565: %\renewcommand{\isasymotimes}{\isamath{\circ}}
haftmann@28565: 
haftmann@28565: 
haftmann@28565: %% content
haftmann@28565: 
haftmann@20946: \title{\includegraphics[scale=0.5]{isabelle_isar}
haftmann@20946:   \\[4ex] Haskell-style type classes with Isabelle/Isar}
haftmann@20946: \author{\emph{Florian Haftmann}}
haftmann@20946: 
haftmann@20946: \begin{document}
haftmann@20946: 
haftmann@20946: \maketitle
haftmann@20946: 
haftmann@20946: \begin{abstract}
haftmann@20946:   This tutorial introduces the look-and-feel of Isar type classes
haftmann@20946:   to the end-user; Isar type classes are a convenient mechanism
haftmann@20946:   for organizing specifications, overcoming some drawbacks
haftmann@20946:   of raw axiomatic type classes. Essentially, they combine
haftmann@20946:   an operational aspect (in the manner of Haskell) with
haftmann@20946:   a logical aspect, both managed uniformly.
haftmann@20946: \end{abstract}
haftmann@20946: 
haftmann@20946: \thispagestyle{empty}\clearpage
haftmann@20946: 
haftmann@20946: \pagenumbering{roman}
haftmann@20946: \clearfirst
haftmann@20946: 
haftmann@20946: \input{Thy/document/Classes.tex}
haftmann@20946: 
haftmann@20946: \begingroup
haftmann@20946: %\tocentry{\bibname}
haftmann@20946: \bibliographystyle{plain} \small\raggedright\frenchspacing
haftmann@23956: \bibliography{../../manual}
haftmann@20946: \endgroup
haftmann@20946: 
haftmann@20946: \end{document}
haftmann@20946: 
haftmann@20946: 
haftmann@20946: %%% Local Variables: 
haftmann@20946: %%% mode: latex
haftmann@20946: %%% TeX-master: t
haftmann@20946: %%% End: