--- a/LMCS-Paper/Paper.thy	Fri Sep 09 17:11:38 2011 +0100
+++ b/LMCS-Paper/Paper.thy	Sat Sep 10 00:03:42 2011 +0100
@@ -762,8 +762,10 @@
   \end{equation}\smallskip
   
   \noindent
-  In these relation we replaced the free-atom function @{text "fa"} with @{term "supp"} and the 
-  relation @{text R} with equality. We can show the following properties:
+  Note that in these relation we replaced the free-atom function @{text "fa"}
+  with @{term "supp"} and the relation @{text R} with equality. We can show
+  the following properties:
+
 
   \begin{lem}\label{alphaeq} 
   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$
@@ -1175,11 +1177,11 @@
   clause, and also is used in the definition of the binding function. The
   restriction we have to impose is that the binding function can only return
   free atoms, that is the ones that are not mentioned in a binding clause.
-  Therefore @{text "y"} cannot be used in the binding function, @{text "bn"}
+  Therefore @{text "y"} cannot be used in the binding function @{text "bn"}
   (since it is bound in @{text "ACons"} by the binding clause), but @{text x}
   can (since it is a free atom). This restriction is sufficient for lifting 
-  the binding function to alpha-equated terms. If we would allow that @{text "bn"}
-  can return also @{text "y"}, then it would not be respectful and therefore
+  the binding function to alpha-equated terms. If we would permit that @{text "bn"}
+  can also return @{text "y"}, then it would not be respectful and therefore
   cannot be lifted.
 
   In the version of Nominal Isabelle described here, we also adopted the