--- a/Paper/Paper.thy	Sun Jan 30 16:59:57 2011 +0000
+++ b/Paper/Paper.thy	Sun Jan 30 17:09:02 2011 +0000
@@ -23,7 +23,7 @@
 section {* Preliminaries *}
 
 text {*
-  A central technique in our proof is the solution of equational systems
+  Central to our proof will be the solution of equational systems
   involving regular expressions. For this we will use the following ``reverse'' 
   version of Arden's lemma.
 
@@ -34,14 +34,14 @@
   \end{lemma}
 
   \begin{proof}
-  For right-to-left direction we assume @{thm (rhs) ardens_revised} and show
-  @{thm (lhs) ardens_revised}. From Lemma ??? we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
+  For the right-to-left direction we assume @{thm (rhs) ardens_revised} and show
+  that @{thm (lhs) ardens_revised} holds. From Lemma ??? we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
   which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both 
   sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
-  is @{term "B \<union> (B ;; A\<star>) ;; A"}. This completes this direction. 
+  is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. 
 
   For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction
-  on @{text n}, we can show the property
+  on @{text n}, we can establish the property
 
   \begin{center}
   @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_helper}
@@ -50,9 +50,10 @@
   \noindent
   Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for
   all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using Lemma ???.
-  The inclusion in the other direction we establishing by assuming a string @{text s}
+  For the inclusion in the other direction we assume a string @{text s}
   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)"} as its length is only @{text k}. 
+  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
   @{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