--- a/Journal/Paper.thy	Thu Jul 28 11:56:25 2011 +0000
+++ b/Journal/Paper.thy	Thu Jul 28 14:22:10 2011 +0000
@@ -779,8 +779,8 @@
   \begin{lmm}\label{ardenable}
   Given an equation @{text "X = rhs"}.
   If @{text "X = \<Union>\<calL> ` rhs"},
-  @{thm (prem 2) Arden_keeps_eq}, and
-  @{thm (prem 3) Arden_keeps_eq}, then
+  @{thm (prem 2) Arden_preserves_soundness}, and
+  @{thm (prem 3) Arden_preserves_soundness}, then
   @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
   \end{lmm}
   
@@ -1098,6 +1098,9 @@
   Much more interesting, however, are the inductive cases. They seem hard to solve 
   directly. The reader is invited to try. 
 
+  Constable et al \cite{Constable00} give the following suggestive picture about
+  equivalence classes:
+
   Our first proof will rely on some
   \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will 
   be easy to prove that the \emph{range} of these tagging-functions is finite.