--- a/LMCS-Paper/Paper.thy	Thu Sep 22 21:43:04 2011 +0900
+++ b/LMCS-Paper/Paper.thy	Thu Sep 22 11:42:55 2011 +0200
@@ -724,7 +724,7 @@
 
   If we do not want to make any difference between the order of binders \emph{and}
   also allow vacuous binders, that means according to Pitts~\cite{Pitts04} 
-  \emph{restrict} names, then we keep sets of binders, but drop 
+  \emph{restrict} atoms, then we keep sets of binders, but drop 
   condition {\it (iv)} in Definition~\ref{alphaset}:
 
   \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
@@ -745,7 +745,7 @@
   define
   
   \[
-  @{text "fa(x) \<equiv> {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) \<equiv> fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
+  @{text "fa(x) \<equiv> {x}"}  \hspace{10mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) \<equiv> fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
   \]\smallskip
 
   \noindent
@@ -803,7 +803,7 @@
   \<pi> \<bullet> x) equal supp (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided \mbox{@{term
   "alpha_set_ex (as, x) equal supp(bs, y)"}} holds. From the assumption we
   have a permutation @{text "\<pi>'"} and for the proof obligation use @{text "\<pi> \<bullet>
-  \<pi>'"}. To show then equivariance, we need to `pull out' the permutations,
+  \<pi>'"}. To show equivariance, we need to `pull out' the permutations,
   which is possible since all operators, namely as @{text "#\<^sup>*, -, =, \<bullet>,
   set"} and @{text "supp"}, are equivariant (see
   \cite{HuffmanUrban10}). Finally, we apply the permutation operation on
@@ -923,7 +923,7 @@
   \end{equation}\smallskip
   
   \noindent
-  This is because for every finite sets of atoms, say @{text "bs"}, we have 
+  This is because for every finite set of atoms, say @{text "bs"}, we have 
   @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
   Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
   the first equation of Theorem~\ref{suppabs}. The others are similar.
@@ -1926,7 +1926,7 @@
   \end{equation}\smallskip
 
   \noindent
-  where @{text "y"} is a variable of type @{text "ty"}$_i$ and @{text "P"} is the 
+  where @{text "y"} is a variable of type @{text "ty\<AL>"}$_i$ and @{text "P"} is the 
   property that is established by the case analysis. Similarly, we have a (mutual) 
   induction principle for the types @{text "ty\<AL>"}$_{1..n}$, which is of the 
   form
@@ -1992,7 +1992,7 @@
   \end{equation}\smallskip
 
   By working now completely on the alpha-equated level, we
-  can first show using \eqref{calphaeqvt} that the support of each term
+  can first show using \eqref{calphaeqvt} and Property~\ref{swapfreshfresh} that the support of each term
   constructor is included in the support of its arguments, 
   namely
 
@@ -2112,7 +2112,7 @@
   "x"}$_{1..r}$. The problem with this is that in the presence of binders we cannot make
   any assumptions about the atoms that are bound---for example assuming the variable convention. 
   One obvious way around this
-  problem is to rename them. Unfortunately, this leads to very clunky proofs
+  problem is to rename bound atoms. Unfortunately, this leads to very clunky proofs
   and makes formalisations grievous experiences (especially in the context of 
   multiple bound atoms).
 
@@ -2158,7 +2158,7 @@
   line). In order to see how an instantiation for @{text "c"} in the
   conclusion `controls' the premises, one has to take into account that
   Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated
-  with a pair, for example, then this type-constraint will be propagated to
+  with, for example, a pair, then this type-constraint will be propagated to
   the premises. The main point is that if @{text "c"} is instantiated
   appropriately, then the user can mimic the usual `pencil-and-paper'
   reasoning employing the variable convention about bound and free variables
@@ -2214,7 +2214,7 @@
   the right-hand side) since the weak and strong cases lemma coincide (there
   is no binding in patterns).  Interesting are only the cases for @{text
   "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"}, where we have some binders and
-  therefore have an addition assumption about avoiding @{text "c"}.  Let us
+  therefore have an additional assumption about avoiding @{text "c"}.  Let us
   first establish the case for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma
   \eqref{inductex} we can assume that
 
@@ -2328,7 +2328,7 @@
   \[\mbox{
   \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
   $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
-  $\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+  $\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet>\<^bsub>bn\<^esub> x\<^isub>i"} provided @{text "bn x\<^isub>i"} is in @{text "rhs"}\\
   $\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet> x\<^isub>i"} otherwise
   \end{tabular}}
   \]\smallskip
@@ -2336,7 +2336,7 @@
   \noindent
   Using again the quotient package  we can lift the auxiliary permutation operations
   @{text "_ \<bullet>\<^bsub>bn\<^esub> _"}
-  to 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>"} 
@@ -2384,9 +2384,9 @@
 
   Consequently,  we can discharge all proof-obligations about having covered all
   cases. This completes the proof establishing that the weak induction principles imply 
-  the strong induction principles. These strong induction principles have proved 
-  already to be very useful in practice, particularly for proving properties about 
-  capture-avoiding substitution. 
+  the strong induction principles. These strong induction principles have already proved 
+  being very useful in practice, particularly for proving properties about 
+  capture-avoiding substitution \cite{Urban08}. 
 *}
 
 
@@ -2455,7 +2455,7 @@
   have proved that our definitions lead to alpha-equated terms, whose support
   is as expected (that means bound atoms are removed from the support). We
   also showed that our specifications lift from `raw' types to types of
-  alpha-equivalence classes. For this we had to establish (automatically) that every
+  alpha-equivalence classes. For this we have established (automatically) that every
   term-constructor and function defined for `raw' types 
   is respectful w.r.t.~alpha-equivalence.
 
@@ -2616,7 +2616,7 @@
   in Ott. We have tried out the extension with calculi such as Core-Haskell,
   type-schemes and approximately a dozen of other typical examples from
   programming language research~\cite{SewellBestiary}. The code will
-  eventually become part of the next Isabelle distribution.\footnote{It 
+  eventually become part of the Isabelle distribution.\footnote{It 
   can be downloaded already from \href{http://isabelle.in.tum.de/nominal/download}
   {http://isabelle.in.tum.de/nominal/download}.}