--- a/Paper/document/root.tex	Tue Feb 08 16:49:18 2011 +0000
+++ b/Paper/document/root.tex	Tue Feb 08 18:04:54 2011 +0000
@@ -36,8 +36,8 @@
 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 that they need to be represented as graphs 
-or matrices, neither of which can be defined as inductive datatype. Also 
+theorem provers. The reason is that they need to be represented as graphs, 
+matrices or functions, none of which are inductive datatypes. Also 
 operations, such as disjoint unions of graphs, are not easily formalisiable 
 in HOL. In contrast, regular expressions can be defined conveniently 
 as datatype and a corresponding reasoning infrastructure comes for