--- a/Journal/document/root.tex	Wed Sep 07 18:17:56 2011 +0000
+++ b/Journal/document/root.tex	Thu Sep 08 15:08:02 2011 +0000
@@ -57,7 +57,7 @@
 graphs, matrices and functions are not easily formalisiable in HOL. In contrast, regular
 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
+result from formal language theory---the Myhill-Nerode Theorem---can be
 recreated using only regular expressions. From this theorem many closure
 properties of regular languages follow.
 \end{abstract}