--- a/Paper/Paper.thy	Thu Apr 08 13:04:49 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 08 14:18:38 2010 +0200
@@ -8,7 +8,8 @@
   abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
   alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c"
-  alpha2 :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow> 'f" 
+  Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 
+  
 
 definition
  "equal \<equiv> (op =)" 
@@ -25,12 +26,12 @@
   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
-  alpha2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{\#{}list}}$}}>\<^bsup>_, _, _\<^esup> _") and
   fv ("fv'(_')" [100] 100) and
   equal ("=") and
   alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
   Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and
   Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and
+  Abs_dist ("[_]\<^raw:$\!$>\<^bsub>#list\<^esub>._") and
   Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and
   Cons ("_::_" [78,77] 73) and
   supp_gen ("aux _" [1000] 10) and
@@ -2072,23 +2073,16 @@
 
 
   We have also not yet played with other binding modes. For example we can
-  imagine that there is need for a binding mode \isacommand{bind\_\#list} with an associated
-  alpha-equivalence definition as follows:
+  imagine that there is need for a binding mode \isacommand{bind\_\#list} with
+  an associated abstraction of the form
   %
   \begin{center}
-  $\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{2}{l}{@{term "alpha2 (as, x) R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
-             & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\
-  \wedge     & @{term "(fv(x) - set as) \<sharp>* p"}\\
-  \wedge     & @{text "(p \<bullet> x) R y"}\\
-  \wedge     & @{term "(p \<bullet> as) = bs"}\\
-  \wedge     & @{term "distinct as"} 
-  \end{array}$
+  @{term "Abs_dist as x"}
   \end{center}
 
   \noindent
-  In this definition we added the requirement that all bound variables in a
-  list are distinct. Once we feel confident about such binding modes, our implementation 
+  where instead of lists, we abstract lists of distinct elements.
+  Once we feel confident about such binding modes, our implementation 
   can be easily extended to accommodate them.
 
   \medskip