# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1285931507 14400
# Node ID 4b06b8818415d10d24d315d1f24fe94340f4c79e
# Parent  bcd119bb854b4418c9ddf547263419b60327aead# Parent  074304d56eb2e054075481d81bddc640c0e74a5c
merged

diff -r bcd119bb854b -r 4b06b8818415 Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Oct 01 07:09:59 2010 -0400
+++ b/Paper/Paper.thy	Fri Oct 01 07:11:47 2010 -0400
@@ -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