--- a/Myhill_2.thy	Fri Feb 11 13:30:37 2011 +0000
+++ b/Myhill_2.thy	Sun Feb 13 10:36:53 2011 +0000
@@ -19,18 +19,22 @@
 
 text {*
   The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions.
-  While base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straight forward,
-  the inductive cases are rather involved. What we have when starting to prove these inductive caes is that
-  the partitions induced by the componet language are finite. The basic idea to show the finiteness of the 
-  partition induced by the composite language is to attach a tag @{text "tag(x)"} to every string 
-  @{text "x"}. The tags are made of equivalent classes from the component partitions. Let @{text "tag"}
-  be the tagging function and @{text "Lang"} be the composite language, it can be proved that
-  if strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as:
+  where base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to
+  proof. Real difficulty lies in inductive cases.  By inductive hypothesis, languages defined by
+  sub-expressions induce finite partitiions. Under such hypothsis, we need to prove that the language 
+  defined by the composite regular expression gives rise to finite partion.  
+  The basic idea is to attach a tag @{text "tag(x)"} to every string 
+  @{text "x"}. The tagging fuction @{text "tag"} is carefully devised, which returns tags 
+  made of equivalent classes of the partitions induced by subexpressoins, and therefore has a finite
+  range. Let @{text "Lang"} be the composite language, it is proved that:
+  \begin{quote}
+  If strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as:
   \[
   @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}
   \]
-  then the partition induced by @{text "Lang"} must be finite. There are two arguments for this. 
-  The first goes as the following:
+  then the partition induced by @{text "Lang"} must be finite.
+  \end{quote}
+  There are two arguments for this. The first goes as the following:
   \begin{enumerate}
     \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"} 
           (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}).