--- a/Paper/document/root.tex	Wed Apr 06 08:18:23 2011 +0000
+++ b/Paper/document/root.tex	Tue Apr 19 02:19:56 2011 +0000
@@ -50,7 +50,7 @@
 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
+expressions can be defined conveniently as a 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.
@@ -60,7 +60,7 @@
 
 \input{session}
 
-\mbox{}\\[-10mm]
+%%\mbox{}\\[-10mm]
 \bibliographystyle{plain}
 \bibliography{root}