--- a/Journal/Paper.thy	Mon Sep 12 19:50:21 2011 +0000
+++ b/Journal/Paper.thy	Tue Sep 13 12:00:53 2011 +0000
@@ -2032,8 +2032,8 @@
   "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"}
   give rise to the same partitions. So if one is finite, the other is too, and
   vice versa. As noted earlier, our algorithm for solving equational systems
-  actually calculates the regular expression for the complement language. 
-  Calculating this regular expression via
+  actually calculates a regular expression for the complement language. 
+  Calculating such a regular expression via
   automata using the standard method would be quite involved. It includes the
   steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
   "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}