--- a/Myhill_2.thy	Wed May 04 07:05:59 2011 +0000
+++ b/Myhill_2.thy	Mon May 09 07:25:37 2011 +0000
@@ -661,7 +661,7 @@
         with eq_zab show ?thesis by simp
       qed
       with h5 h6 show ?thesis 
-        by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)
+        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
     qed
   } 
   -- {* By instantiating the reasoning pattern just derived for both directions:*} 
@@ -770,7 +770,7 @@
         with z_decom show ?thesis by auto 
       qed
       with h5 h6 show ?thesis 
-        by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)
+        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
     qed
   } 
   -- {* By instantiating the reasoning pattern just derived for both directions:*} 

--- a/Paper/Paper.thy	Wed May 04 07:05:59 2011 +0000
+++ b/Paper/Paper.thy	Mon May 09 07:25:37 2011 +0000
@@ -513,7 +513,7 @@
   \end{equation}
 
   \noindent
-  The reason for adding the @{text \<lambda>}-marker to our initial equational system is 
+  holds. The reason for adding the @{text \<lambda>}-marker to our initial equational system is 
   to obtain this equation: it only holds with the marker, since none of 
   the other terms contain the empty string. The point of the initial equational system is
   that solving it means we will be able to extract a regular expression for every equivalence class. 
@@ -721,7 +721,7 @@
  
   \noindent
   The first two ensure that the equational system is always finite (number of equations
-  and number of terms in each equation); the second makes sure the `meaning' of the 
+  and number of terms in each equation); the third makes sure the `meaning' of the 
   equations is preserved under our transformations. The other properties are a bit more
   technical, but are needed to get our proof through. Distinctness states that every
   equation in the system is distinct. @{text Ardenable} ensures that we can always
@@ -875,7 +875,7 @@
 
 text {*
   We will prove in this section the second part of the Myhill-Nerode
-  theorem. It can be formulated in our setting as follows.
+  theorem. It can be formulated in our setting as follows:
 
   \begin{theorem}
   Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.