--- a/Paper/document/root.tex	Wed Feb 02 15:43:22 2011 +0000
+++ b/Paper/document/root.tex	Thu Feb 03 05:38:47 2011 +0000
@@ -35,9 +35,9 @@
 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 they need to be represented as graphs 
-or matrices, neither of which can be easily defined as datatype. Also 
-operations, such as disjoint union of graphs, are not easily formalisiable 
+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 
 as datatype and a corresponding reasoning infrastructure comes for 
 free. We show in this paper that a central result from formal