--- a/Paper/Paper.thy	Wed Sep 29 09:51:57 2010 -0400
+++ b/Paper/Paper.thy	Fri Oct 01 15:44:50 2010 +0900
@@ -783,9 +783,9 @@
   Assuming @{text x} has finite support, then\\[-6mm] 
   \begin{center}
   \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\
-  @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\
-  @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}
+  @{thm (lhs) supp_Abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(1)[no_vars]}\\
+  @{thm (lhs) supp_Abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(2)[no_vars]}\\
+  @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}
   \end{tabular}
   \end{center}
   \end{thm}
@@ -796,8 +796,8 @@
   we have 
   %
   \begin{equation}\label{abseqiff}
-  @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; 
-  @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+  @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; 
+  @{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
   \end{equation}
 
   \noindent
@@ -814,7 +814,7 @@
   the following lemma about swapping two atoms in an abstraction.
   
   \begin{lemma}
-  @{thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
+  @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
   \end{lemma}
 
   \begin{proof}
@@ -828,7 +828,7 @@
   with \eqref{absperm} allows us to show
   %
   \begin{equation}\label{halfone}
-  @{thm abs_supports(1)[no_vars]}
+  @{thm Abs_supports(1)[no_vars]}
   \end{equation}
   
   \noindent
@@ -856,7 +856,7 @@
   we further obtain
   %
   \begin{equation}\label{halftwo}
-  @{thm (concl) supp_abs_subset1(1)[no_vars]}
+  @{thm (concl) Abs_supp_subset1(1)[no_vars]}
   \end{equation}
 
   \noindent