--- a/Paper/Paper.thy	Sat Mar 05 11:42:14 2011 +0000
+++ b/Paper/Paper.thy	Tue Mar 15 11:04:53 2011 +0000
@@ -914,7 +914,7 @@
   \end{center}
   \end{definition}
 
-  \noindent
+
   In order to establish finiteness of a set @{text A}, we shall use the following powerful
   principle from Isabelle/HOL's library.
   %
@@ -1218,7 +1218,7 @@
    @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and
   @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
   such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the
-  `border' of @{text x} and @{text z}. This string is @{text "(x - x') @ z\<^isub>a"}.
+  `border' of @{text x} and @{text z}. This string is @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a"}.
 
   In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
   the following tagging-function:
@@ -1272,8 +1272,8 @@
 text {*
   In this paper we took the view that a regular language is one where there
   exists a regular expression that matches all of its strings. Regular
-  expressions can conveniently be defined as a datatype in a HOL-based theorem
-  prover. For us it was therefore interesting to find out how far we can push
+  expressions can conveniently be defined as a datatype in HOL-based theorem
+  provers. For us it was therefore interesting to find out how far we can push
   this point of view. We have established both directions of the Myhill-Nerode
   theorem.
   %