--- a/Paper/Paper.thy	Sun Jan 30 17:21:53 2011 +0000
+++ b/Paper/Paper.thy	Sun Jan 30 17:24:37 2011 +0000
@@ -56,7 +56,7 @@
   with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised}
   we know that @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
   (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). 
-  From @{text "(*)"} it follows that
+  From @{text "(*)"} it follows then that
   @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
   implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this
   is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed