
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{graphicx,../iman,../extra,../isar,../pdfsetup}
\usepackage{generated/isabelle,generated/isabellesym}

\newcommand{\isasymOtimes}{\emph{$\odot$}}
\newcommand{\isasymOplus}{\emph{$\oplus$}}
\newcommand{\isasyminv}{\emph{${}^{-1}$}}
\newcommand{\isasymunit}{\emph{$1$}}
\newcommand{\TIMES}{\odot}
\newcommand{\PLUS}{\oplus}


\newcommand{\secref}[1]{\S\ref{#1}}
\newcommand{\figref}[1]{figure~\ref{#1}}

\hyphenation{Isabelle}
\hyphenation{Isar}
\hyphenation{Haskell}

\title{\includegraphics[scale=0.5]{isabelle_isar}
  \\[4ex] Using Axiomatic Type Classes in Isabelle}
\author{\emph{Markus Wenzel} \\ TU M\"unchen}


\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

\pagestyle{headings}
\sloppy
\binperiod     %%%treat . like a binary operator


\begin{document}

\underscoreoff

\maketitle 

\begin{abstract}
  Isabelle offers order-sorted type classes on top of the simple types of
  plain Higher-Order Logic.  The resulting type system is similar to that of
  the programming language Haskell.  Its interpretation within the logic
  enables further application, though, apart from restricting polymorphism
  syntactically.  In particular, the concept of \emph{Axiomatic Type Classes}
  provides a useful light-weight mechanism for hierarchically-structured
  abstract theories. Subsequently, we demonstrate typical uses of Isabelle's
  axiomatic type classes to model basic algebraic structures.
  
  Note that this document describes axiomatic type classes using Isabelle/Isar
  theories, with proofs expressed via Isar proof language elements.  The new
  theory format greatly simplifies the arrangement of the overall development,
  since definitions and proofs may be freely intermixed.  Users who prefer
  tactic scripts over structured proofs do not need to fall back on separate
  ML scripts, but may refer to Isar's tactic emulation commands.
\end{abstract}


\pagenumbering{roman} \tableofcontents \clearfirst

\include{body}

%FIXME
\nocite{nipkow-types93}
\nocite{nipkow-sorts93}
\nocite{Wenzel:1997:TPHOL}
\nocite{paulson-isa-book}
\nocite{isabelle-isar-ref}
\nocite{Wenzel:1999:TPHOL}

\begingroup
  \bibliographystyle{plain} \small\raggedright\frenchspacing
  \bibliography{../manual}
\endgroup

\end{document}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
% LocalWords:  Isabelle FIXME
