--- a/LMCS-Paper/Paper.thy	Wed Sep 21 15:18:32 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 18:27:24 2011 +0200
@@ -2177,7 +2177,7 @@
   principle. Once these two proof obligations are discharged, the reasoning
   infrastructure of the function package will automatically derive the
   stronger induction principle. This way of establishing the stronger induction
-  principle is considerably simpler than the earlier work presented \cite{Urban08}.
+  principle is considerably simpler than the earlier work presented in \cite{Urban08}.
 
   As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,
   which we lifted in the previous section and which are all well-founded. It
@@ -2207,7 +2207,7 @@
   \noindent
   They are stronger in the sense that they allow us to assume in the @{text
   "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms
-  avoid a context @{text "c"} (which is assumed to be finitely supported).
+  avoid, or being fresh for, a context @{text "c"} (which is assumed to be finitely supported).
   
   These stronger cases lemmas can be derived from the `weak' cases lemmas
   given in \eqref{inductex}. This is trivial in case of patterns (the one on
@@ -2234,7 +2234,7 @@
   which we must use in order to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
   use this implication directly, because we have no information whether or not @{text
   "x\<^isub>1"} is fresh for @{text "c"}.  However, we can use Properties
-  \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: we know
+  \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}. We know
   by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\<alpha>
   x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 -
   {atom x\<^isub>1}"}). Property \ref{avoiding} provides us then with a
@@ -2310,7 +2310,7 @@
   that @{text "\<pi>"} only renames atoms that become bound. In this way @{text "\<pi>"}
   does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"} (which only tracks alpha-equivalence of terms that are not
   under the binder). However, the problem is that the
-  permutation operation @{text "\<pi> \<bullet> x\<^isub>1"} applies to all attoms in @{text "x\<^isub>1"}. To avoid this
+  permutation operation @{text "\<pi> \<bullet> x\<^isub>1"} applies to all atoms in @{text "x\<^isub>1"}. To avoid this
   we introduce an auxiliary permutation operations, written @{text "_
   \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or
   more precisely the atoms specified by the @{text "bn"}-functions) and leaves
@@ -2336,7 +2336,7 @@
   \noindent
   Using again the quotient package  we can lift the auxiliary permutation operations
   @{text "_ \<bullet>\<^bsub>bn\<^esub> _"}
-  alpha-equated terms. Moreover we can prove the following two properties
+  to alpha-equated terms. Moreover we can prove the following two properties
 
   \begin{lem}\label{permutebn} 
   Given a binding function @{text "bn\<^sup>\<alpha>"} and auxiliary equivalence @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"} 
@@ -2355,7 +2355,7 @@
   is equivalent to first permuting the binders and then calculating the bound
   atoms. The second states that @{text "_ \<bullet>\<AL>\<^bsub>bn\<^esub> _"} preserves
   @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}.  The main point of the auxiliary
-  permutation functions is that they allow us to rename just the binders in a
+  permutation functions is that they allow us to rename just the bound atoms in a
   term, without changing anything else.
   
   Having the auxiliary permutation function in place, we can now solve all remaining cases. 
@@ -2654,7 +2654,7 @@
   imagine that there is need for a binding mode where instead of usual lists,
   we abstract lists of distinct elements (the corresponding type @{text
   "dlist"} already exists in the library of Isabelle/HOL). We expect the
-  presented work can be easily extended to accommodate such binding modes.\medskip
+  presented work can be extended to accommodate such binding modes.\medskip
   
   \noindent
   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many