# HG changeset patch
# User urbanc
# Date 1296408277 0
# Node ID da85feadb8e329cf2d2fd85673d2540ac211484d
# Parent  4a517c6ac07d2dac34f7ab72b86f8e9a00a2cbd9
small typo

diff -r 4a517c6ac07d -r da85feadb8e3 Paper/Paper.thy
--- 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