--- a/Paper/document/root.tex	Thu Feb 03 05:38:47 2011 +0000
+++ b/Paper/document/root.tex	Thu Feb 03 09:54:19 2011 +0000
@@ -38,7 +38,7 @@
 theorem provers. The reason is that they need to be represented as graphs 
 or matrices, neither of which can be defined as inductive datatype. Also 
 operations, such as disjoint unions of graphs, are not easily formalisiable 
-in HOL. In contrast, regular expressions can be defined easily 
+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