diff -r bdb1eab47161 -r 894599a50af3 Paper/Paper.thy
--- a/Paper/Paper.thy	Sat Sep 04 07:28:35 2010 +0800
+++ b/Paper/Paper.thy	Sat Sep 04 07:39:38 2010 +0800
@@ -21,21 +21,21 @@
   supp ("supp _" [78] 73) and
   uminus ("-_" [78] 73) and
   If  ("if _ then _ else _" 10) and
-  alpha_gen ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
+  alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
   alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
   alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
   fv ("fa'(_')" [100] 100) and
   equal ("=") and
-  alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
-  Abs ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
+  alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
+  Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
   Abs_lst ("[_]\<^bsub>list\<^esub>._") and
   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
   Abs_res ("[_]\<^bsub>res\<^esub>._") and
   Abs_print ("_\<^bsub>set\<^esub>._") and
   Cons ("_::_" [78,77] 73) and
-  supp_gen ("aux _" [1000] 10) and
+  supp_set ("aux _" [1000] 10) and
   alpha_bn ("_ \<approx>bn _")
 
 consts alpha_trm ::'a
@@ -647,7 +647,7 @@
   %
   \begin{equation}\label{alphaset}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
-  \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+  \multicolumn{3}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
               & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
   @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
   @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
@@ -730,7 +730,7 @@
   types. For this we define 
   %
   \begin{equation}
-  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
+  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
   \end{equation}
   
   \noindent
@@ -762,7 +762,7 @@
   The elements in these types will be, respectively, written as:
 
   \begin{center}
-  @{term "Abs as x"} \hspace{5mm} 
+  @{term "Abs_set as x"} \hspace{5mm} 
   @{term "Abs_res as x"} \hspace{5mm}
   @{term "Abs_lst as x"} 
   \end{center}
@@ -832,7 +832,7 @@
   function @{text aux}, taking an abstraction as argument:
   %
   \begin{center}
-  @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
+  @{thm supp_set.simps[THEN eq_reflection, no_vars]}
   \end{center}
   
   \noindent
@@ -842,7 +842,7 @@
   This in turn means
   %
   \begin{center}
-  @{term "supp (supp_gen (Abs as x)) \<subseteq> supp (Abs as x)"}
+  @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
   \end{center}
 
   \noindent
@@ -860,7 +860,7 @@
   Theorem~\ref{suppabs}. 
 
   The method of first considering abstractions of the
-  form @{term "Abs as x"} etc is motivated by the fact that 
+  form @{term "Abs_set as x"} etc is motivated by the fact that 
   we can conveniently establish  at the Isabelle/HOL level
   properties about them.  It would be
   laborious to write custom ML-code that derives automatically such properties 
@@ -1489,7 +1489,7 @@
   lets us formally define the premise @{text P} for a non-empty binding clause as:
   %
   \begin{center}
-  \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
+  \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.
   \end{center}
 
   \noindent