\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\newcommand{\isasymemdash}{-}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{Category Theory}
\author{Alexander Katovsky}
\maketitle

\begin{abstract}
This article presents a development of Category Theory in Isabelle.  A
Category is defined using records and locales in Isabelle/HOL.  Functors and
Natural Transformations are also defined.  The main result that has been
formalized is that the Yoneda functor is a full and faithful embedding.  We
also formalize the completeness of many sorted monadic equational logic.
Extensive use is made of the HOLZF theory in both cases.
For an informal description see~\cite{apk}.
\end{abstract}

\tableofcontents

% include generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
