--- a/Paper/document/root.tex	Fri Feb 18 14:26:23 2011 +0000
+++ b/Paper/document/root.tex	Fri Feb 18 15:06:06 2011 +0000
@@ -38,8 +38,8 @@
 \begin{abstract} 
 There are numerous textbooks on regular languages. Nearly all of them
 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
+side a connection with regular expressions. Unfortunately, automata are difficult
+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