--- a/Paper/Paper.thy	Thu Feb 10 08:40:38 2011 +0000
+++ b/Paper/Paper.thy	Thu Feb 10 12:32:45 2011 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Myhill" "LaTeXsugar"
+imports "../Myhill" "LaTeXsugar" 
 begin
 
 declare [[show_question_marks = false]]
@@ -499,20 +499,28 @@
   \noindent
   which we also lift to entire right-hand sides of equations, written as
   @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
-  the \emph{arden-operation}, which takes an equivalence class @{text X} and
-  a rhs of an equation.
-
+  the \emph{arden-operation} for an equation of the form @{text "X = rhs"}:
+  
   \begin{center}
-  @{thm arden_op_def}
+  \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+  @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\ 
+   & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+   & & @{text "r' ="}   & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
+   & &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\ 
+  \end{tabular}
   \end{center}
 
   \noindent
-  The term left of $\triangleright$ deletes all terms of the form @{text "(X, r)"};
-  the term on the right calculates first the combinded regular expressions for all
-  @{text r} in the @{text "(X, r)"}, forms the star and appends it to the remaining
-  terms in the @{text rhs}. It can be easily seen that this operation mimics Arden's
-  lemma on the level of equations.
+  We first delete all terms of the form @{text "(X, r)"} from @{text rhs};
+  then we calculate the combinded regular expressions for all @{text r} coming 
+  from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
+  finally we append this regular expression to @{text rhs'}. It can be easily seen 
+  that this operation mimics Arden's lemma on the level of equations.
   
+
+  \begin{center}
+  @{thm Subst_def}
+  \end{center}
 *}
 
 section {* Regular Expressions Generate Finitely Many Partitions *}