--- a/Paper/Paper.thy	Thu May 12 05:55:05 2011 +0000
+++ b/Paper/Paper.thy	Wed May 18 19:54:43 2011 +0000
@@ -12,9 +12,8 @@
 abbreviation
   "EClass x R \<equiv> R `` {x}"
 
-abbreviation 
-  "append_rexp2 r_itm r \<equiv> append_rexp r r_itm"
-
+abbreviation
+  "Append_rexp2 r_itm r == Append_rexp r r_itm"
 
 notation (latex output)
   str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
@@ -32,8 +31,9 @@
   EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
   transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
   Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
-  append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
-  append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
+  Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
+  Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
+  
   uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
   tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
   tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
@@ -494,8 +494,8 @@
   
   \begin{center}
   @{text "\<calL>(Y, r) \<equiv>"} %
-  @{thm (rhs) 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]}
+  @{thm (rhs) L_rhs_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+  @{thm L_rhs_trm.simps(1)[where r="r", THEN eq_reflection]}
   \end{center}
 
   \noindent
@@ -561,13 +561,13 @@
   we define the \emph{append-operation} taking a term and a regular expression as argument
 
   \begin{center}
-  @{thm append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
-  @{thm append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+  @{thm Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+  @{thm Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
   \end{center}
 
   \noindent
   We lift this operation to entire right-hand sides of equations, written as
-  @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
+  @{thm (lhs) Append_rexp_rhs_def[where rexp="r"]}. With this we can define
   the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
   %
   \begin{equation}\label{arden_def}
@@ -712,10 +712,10 @@
       @{term "finite ES"} & @{text "(finiteness)"}\\
   & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
   & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
-  & @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\
+  & @{text "\<and>"} & @{thm (rhs) distinctness_def}\\
   &             &  & @{text "(distinctness)"}\\
   & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\   
-  & @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\
+  & @{text "\<and>"} & @{thm (rhs) validity_def} & @{text "(validity)"}\\
   \end{tabular}
   \end{center}