--- a/Journal/document/root.tex	Wed Aug 03 17:08:31 2011 +0000
+++ b/Journal/document/root.tex	Fri Aug 05 05:34:11 2011 +0000
@@ -54,7 +54,7 @@
 to formalise 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
+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