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

% 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{The Myhill-Nerode Theorem\\ Based on Regular Expressions}
\author{Chunhan Wu, Xingyuan Zhang and Christian Urban}
\maketitle

\begin{abstract}
There are many proofs of the Myhill-Nerode theorem using automata. In this
library we give a proof entirely based on regular expressions, since
regularity of languages can be conveniently defined using regular expressions
(it is more painful in HOL to define regularity in terms of automata).  We
prove the first direction of the Myhill-Nerode theorem by solving equational
systems that involve regular expressions.  For the second direction we give two
proofs: one using tagging-functions and another using partial derivatives. We
also establish various closure properties of regular languages.\footnote{Most
details of the theories are described in the paper \cite{WuZhangUrban11}.}
\end{abstract}

\tableofcontents
\bigskip

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

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
