diff -r 1a14c4171a51 -r 4e5a7b606eab Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Jun 10 14:53:28 2010 +0200
+++ b/Paper/Paper.thy	Thu Jun 10 14:53:45 2010 +0200
@@ -115,7 +115,9 @@
   that can be used to faithfully represent this kind of binding in Nominal
   Isabelle.  The difficulty of finding the right notion for alpha-equivalence
   can be appreciated in this case by considering that the definition given by
-  Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
+  Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). A related
+  notion of alpha-equivalence that allows vacuous binders, there called weakening 
+  of contexts, is defined in for the $\Pi\Sigma$-calculus \cite{Altenkirch10}.
 
   However, the notion of alpha-equivalence that is preserved by vacuous
   binders is not always wanted. For example in terms like
@@ -154,7 +156,7 @@
   \begin{center}
   @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}
   \end{center}
-
+  %
   \noindent
   As a result, we provide three general binding mechanisms each of which binds
   multiple variables at once, and let the user chose which one is intended
@@ -364,9 +366,8 @@
   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
   proofs, we establish a reasoning infrastructure for alpha-equated
   terms, including properties about support, freshness and equality
-  conditions for alpha-equated terms. We are also able to derive, for the moment 
-  only manually, strong induction principles that 
-  have the variable convention already built in.
+  conditions for alpha-equated terms. We are also able to derive strong 
+  induction principles that have the variable convention already built in.
 
   \begin{figure}
   \begin{boxedminipage}{\linewidth}
@@ -2017,11 +2018,20 @@
   inter-translated, but we have not proved this. However, we believe the
   binding specifications in the style of Ott are a more natural way for 
   representing terms involving bindings. Pottier gives a definition for 
-  alpha-equivalence, which is similar to our binding mod \isacommand{bind}. 
+  alpha-equivalence, which is similar to our binding mode \isacommand{bind}. 
   Although he uses also a permutation in case of abstractions, his
   definition is rather different from ours. He proves that his notion
   of alpha-equivalence is indeed a equivalence relation, but a complete
   reasoning infrastructure is well beyond the purposes of his language. 
+  In a slightly different domain (programming with dependent types), the 
+  paper \cite{Altenkirch10} presents a calculus with a notion of 
+  alpha-equivalence related to our binding mode \isacommand{bind\_res}.
+  This definition is similar to the one by Pottier, except that it
+  has a more operational flavour and calculates a partial (renaming) map. 
+  In this way they can handle vacous binders. However, their notion of
+  equality between terms also includes rules for $\beta$ and to our
+  knowledge no concrete mathematical result concerning their notion
+  of equality has been proved.    
 *}
 
 section {* Conclusion *}