--- a/Paper/document/root.tex	Wed Feb 09 04:54:23 2011 +0000
+++ b/Paper/document/root.tex	Wed Feb 09 06:09:46 2011 +0000
@@ -10,6 +10,8 @@
 \usepackage{times}
 \usepackage{proof}
 \usepackage{stmaryrd}
+\usepackage{mathabx}
+
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -32,18 +34,18 @@
 \maketitle
 
 \begin{abstract} 
-There are numerous textbooks on regular languages. Nearly all of them 
-introduce the subject by describing finite automata and 
-only mentioning on the side a connection with regular expressions. 
-Unfortunately, automata are a hassle for formalisations in HOL-based
-theorem provers. The reason is that they need to be represented as graphs, 
-matrices or functions, none of which are inductive datatypes. Also 
-operations, such as disjoint unions of graphs, are not easily formalisiable 
-in HOL. In contrast, regular expressions can be defined conveniently 
-as datatype and a corresponding reasoning infrastructure comes for 
-free. We show in this paper that a central result from formal 
-language theory---the Myhill-Nerode theorem---can be recreated 
-using only regular expressions. 
+There are numerous textbooks on regular languages. Nearly all of them
+introduce the subject by describing finite automata and only mentioning on the
+side a connection with regular expressions. Unfortunately, automata are a
+hassle for formalisations in HOL-based theorem provers. The reason is that
+they need to be represented as graphs, matrices or functions, none of which
+are inductive datatypes. Also convenient operations for disjoint unions of
+graphs and functions are not easily formalisiable in HOL. In contrast, regular
+expressions can be defined conveniently as datatype and a corresponding
+reasoning infrastructure comes for free. We show in this paper that a central
+result from formal language theory---the Myhill-Nerode theorem---can be
+recreated using only regular expressions.
+
 \end{abstract}