--- a/Journal/Paper.thy	Tue Mar 06 11:30:45 2012 +0000
+++ b/Journal/Paper.thy	Fri Apr 13 13:12:43 2012 +0000
@@ -618,7 +618,7 @@
   The key definition in the Myhill-Nerode Theorem is the
   \emph{Myhill-Nerode Relation}, which states that w.r.t.~a language two 
   strings are related, provided there is no distinguishing extension in this
-  language. This can be defined as a tertiary relation.
+  language. This can be defined as a ternary relation.
 
   \begin{dfntn}[Myhill-Nerode Relation]\label{myhillneroderel} 
   Given a language @{text A}, two strings @{text x} and
@@ -690,7 +690,7 @@
   \end{equation}
 
   \noindent
-  which means that if we concatenate the character @{text c} to the end of all 
+  which means that if we append the character @{text c} to the end of all 
   strings in the equivalence class @{text Y}, we obtain a subset of 
   @{text X}. Note that we do not define an automaton here, we merely relate two sets
   (with the help of a character). In our concrete example we have 
@@ -703,7 +703,7 @@
   an informal description of this construction. Suppose we have 
   the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
   contains the empty string @{text "[]"} (since equivalence classes are disjoint).
-  Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
+  Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following initial equational system
   
   \begin{center}
   \begin{tabular}{rcl}
@@ -715,7 +715,8 @@
   \end{center}
 
   \noindent
-  where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"}
+  where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} are pairs consiting of an equivalence class and
+  a regular expression. In the initial equational system, they
   stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
   X\<^isub>i"}. 
   %The intuition behind the equational system is that every 
@@ -897,7 +898,9 @@
   \noindent
   Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
   but we can still ensure that it holds throughout our algorithm of transforming equations
-  into solved form. The \emph{substitution-operation} takes an equation
+  into solved form. 
+
+  The \emph{substitution-operation} takes an equation
   of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
 
   \begin{center}
@@ -1603,7 +1606,7 @@
   %
   \begin{center}
   @{thm (lhs) tag_Star_def[where ?A="A", THEN meta_eq_app]}~@{text "\<equiv>"}~
-  @{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>s, x\<^isub>p) \<in> Partitions x}"}
+  @{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"}
   \end{center}
 
   \begin{proof}[@{const Star}-Case]

--- a/Myhill_2.thy	Tue Mar 06 11:30:45 2012 +0000
+++ b/Myhill_2.thy	Fri Apr 13 13:12:43 2012 +0000
@@ -1,3 +1,4 @@
+(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *)
 theory Myhill_2
   imports Myhill_1 "~~/src/HOL/Library/List_Prefix"
 begin
@@ -56,7 +57,7 @@
         by (simp) (blast)
       with X_in Y_in 
       have "X = Y"
-	unfolding quotient_def tag_eq_def by auto
+        unfolding quotient_def tag_eq_def by auto
     } 
     then show "inj_on ?f ?A" unfolding inj_on_def by auto
   qed
@@ -324,7 +325,7 @@
   "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> max \<in> A. \<forall> a \<in> A. length a \<le> length max"
 apply(induct rule:finite.induct)
 apply(simp)
-by (metis (full_types) all_not_in_conv insert_iff linorder_linear order_trans)
+by (metis (hide_lams, no_types) all_not_in_conv insert_iff linorder_le_cases order_trans)
 
 lemma finite_strict_prefix_set: 
   shows "finite {xa. xa < (x::'a list)}"