diff -r a3e0056c228b -r 6457e668dee5 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 09 03:52:28 2011 +0000
+++ b/Paper/Paper.thy	Wed Feb 09 04:50:18 2011 +0000
@@ -238,24 +238,24 @@
   version of Arden's lemma.
 
   \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
-  If @{thm (prem 1) ardens_revised} then
-  @{thm (lhs) ardens_revised} has the unique solution
-  @{thm (rhs) ardens_revised}.
+  If @{thm (prem 1) arden} then
+  @{thm (lhs) arden} has the unique solution
+  @{thm (rhs) arden}.
   \end{lemma}
 
   \begin{proof}
-  For the right-to-left direction we assume @{thm (rhs) ardens_revised} and show
-  that @{thm (lhs) ardens_revised} holds. From Prop.~\ref{langprops}@{text "(i)"} 
+  For the right-to-left direction we assume @{thm (rhs) arden} and show
+  that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"} 
   we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
   which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both 
   sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
   is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. 
 
-  For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction
+  For the other direction we assume @{thm (lhs) arden}. By a simple induction
   on @{text n}, we can establish the property
 
   \begin{center}
-  @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_helper}
+  @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
   \end{center}
   
   \noindent
@@ -263,7 +263,7 @@
   all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using the definition
   of @{text "\<star>"}.
   For the inclusion in the other direction we assume a string @{text s}
-  with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised}
+  with length @{text k} is element in @{text X}. Since @{thm (prem 1) arden}
   we know by Prop.~\ref{langprops}@{text "(ii)"} that 
   @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
   (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). 
@@ -392,8 +392,8 @@
   equational system as follows
   
   \begin{center}
-  @{thm L_rhs_e.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
-  @{thm L_rhs_e.simps(1)[where r="r", THEN eq_reflection]}
+  @{thm L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+  @{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]}
   \end{center}
 
   \noindent