--- a/Journal/Paper.thy	Wed Jul 27 12:32:28 2011 +0000
+++ b/Journal/Paper.thy	Wed Jul 27 15:29:39 2011 +0000
@@ -369,6 +369,7 @@
   @{term "A \<up> n"}. They are defined as usual
 
   \begin{center}
+  
   @{thm conc_def'[THEN eq_reflection, where A1="A" and B1="B"]}
   \hspace{7mm}
   @{thm lang_pow.simps(1)[THEN eq_reflection, where A1="A"]}
@@ -403,7 +404,8 @@
 
 
   Central to our proof will be the solution of equational systems
-  involving equivalence classes of languages. For this we will use Arden's Lemma \cite{Brzozowski64},
+  involving equivalence classes of languages. For this we will use Arden's Lemma 
+  (see \cite[Page 100]{Sakarovitch09}),
   which solves equations of the form @{term "X = A \<cdot> X \<union> B"} provided
   @{term "[] \<notin> A"}. However we will need the following `reverse' 
   version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A \<cdot> X"} to
@@ -449,27 +451,24 @@
   Regular expressions are defined as the inductive datatype
 
   \begin{center}
-  @{text r} @{text "::="}
-  @{term ZERO}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
-  @{term ONE}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
-  @{term "ATOM c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
-  @{term "TIMES r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
-  @{term "PLUS r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
-  @{term "STAR r"}
+  \begin{tabular}{rcl}
+  @{text r} & @{text "::="} & @{term ZERO}\\
+   & @{text"|"} & @{term ONE}\\ 
+   & @{text"|"} & @{term "ATOM c"}\\
+   & @{text"|"} & @{term "TIMES r r"}\\
+   & @{text"|"} & @{term "PLUS r r"}\\
+   & @{text"|"} & @{term "STAR r"}
+  \end{tabular}
   \end{center}
 
   \noindent
   and the language matched by a regular expression is defined as
 
   \begin{center}
-  \begin{tabular}{c@ {\hspace{10mm}}c}
-  \begin{tabular}{rcl}
+  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
   @{thm (lhs) lang.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(1)}\\
   @{thm (lhs) lang.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(2)}\\
   @{thm (lhs) lang.simps(3)[where a="c"]} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(3)[where a="c"]}\\
-  \end{tabular}
-  &
-  \begin{tabular}{rcl}
   @{thm (lhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
        @{thm (rhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
   @{thm (lhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
@@ -477,7 +476,6 @@
   @{thm (lhs) lang.simps(6)[where r="r"]} & @{text "\<equiv>"} &
       @{thm (rhs) lang.simps(6)[where r="r"]}\\
   \end{tabular}
-  \end{tabular}
   \end{center}
 
   Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating 
@@ -526,9 +524,11 @@
   as follows
   
   \begin{center}
-  @{text "X\<^isub>1 = {[]}"}\hspace{5mm}
-  @{text "X\<^isub>2 = {[c]}"}\hspace{5mm}
+  \begin{tabular}{l}
+  @{text "X\<^isub>1 = {[]}"}\\
+  @{text "X\<^isub>2 = {[c]}"}\\
   @{text "X\<^isub>3 = UNIV - {[], [c]}"}
+  \end{tabular}
   \end{center}
 
   One direction of the Myhill-Nerode theorem establishes 
@@ -984,7 +984,7 @@
   we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the @{text Arden} operation
   removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
   This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
-  So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = L (\<Uplus>rs)"}.
+  So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = lang (\<Uplus>rs)"}.
   With this we can conclude the proof.
   \end{proof}
 
@@ -999,7 +999,7 @@
   in @{term "finals A"} there exists a regular expression. Moreover by assumption 
   we know that @{term "finals A"} must be finite, and therefore there must be a finite
   set of regular expressions @{text "rs"} such that
-  @{term "\<Union>(finals A) = L (\<Uplus>rs)"}.
+  @{term "\<Union>(finals A) = lang (\<Uplus>rs)"}.
   Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"} 
   as the regular expression that is needed in the theorem.
   \end{proof}