--- a/Paper/Paper.thy	Thu Feb 10 13:10:16 2011 +0000
+++ b/Paper/Paper.thy	Thu Feb 10 21:00:40 2011 +0000
@@ -373,7 +373,7 @@
   the language is regular. In our setting we therefore have to show:
   
   \begin{theorem}\label{myhillnerodeone}
-  @{thm[mode=IfThen] hard_direction}
+  @{thm[mode=IfThen] Myhill_Nerode1}
   \end{theorem}
 
   \noindent
@@ -534,6 +534,19 @@
   regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
   the substitution operation we will arrange it so that @{text "xrhs"} does not contain
   any occurence of @{text X}.
+
+  We lift these two operation to work over equational systems @{text ES}: @{const Subst_all}
+  substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES}; 
+  @{const Remove} completely removes such an equaution from @{text ES} by substituting 
+  it to the rest of the equational system, but first removing all recursive occurences
+  of @{text X} by applying @{const Arden} to @{text "xrhs"}.
+
+  \begin{center}
+  \begin{tabular}{rcl}
+  @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\
+  @{thm (lhs) Remove_def}    & @{text "\<equiv>"} & @{thm (rhs) Remove_def}
+  \end{tabular}
+  \end{center}
 *}
 
 section {* Regular Expressions Generate Finitely Many Partitions *}