--- a/Paper/Paper.thy	Thu May 13 16:09:34 2010 +0100
+++ b/Paper/Paper.thy	Thu May 13 17:41:28 2010 +0100
@@ -344,8 +344,8 @@
   alpha-equivalence and therefore cannot be lifted. To sum up, every lifting
   of theorems to the quotient level needs proofs of some respectfulness
   properties (see \cite{Homeier05}). In the paper we show that we are able to
-  automate these proofs and therefore can establish a reasoning infrastructure
-  for alpha-equated terms.
+  automate these proofs and as a result can automatically establish a reasoning 
+  infrastructure for alpha-equated terms.
 
   The examples we have in mind where our reasoning infrastructure will be
   helpful includes the term language of System @{text "F\<^isub>C"}, also
@@ -563,7 +563,7 @@
   @{text "x R y"} \;\;implies\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
   \end{center}
 
-  Finally, the nominal logic work provides us with convenient means to rename 
+  Finally, the nominal logic work provides us with general means to rename 
   binders. While in the older version of Nominal Isabelle, we used extensively 
   Property~\ref{swapfreshfresh} for renaming single binders, this property 
   proved unwieldy for dealing with multiple binders. For such binders the 
@@ -590,7 +590,7 @@
   fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 
   @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
 
-  Most properties given in this section are described in \cite{HuffmanUrban10}
+  Most properties given in this section are described in detail in \cite{HuffmanUrban10}
   and of course all are formalised in Isabelle/HOL. In the next sections we will make 
   extensively use of these properties in order to define alpha-equivalence in 
   the presence of multiple binders.
@@ -610,7 +610,7 @@
   on the user-level of Isabelle/HOL, as opposed to write custom ML-code that
   generates them anew for each specification. To that end, we will consider
   first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs
-  are intended to represent the abstraction, or binding, of the set @{text
+  are intended to represent the abstraction, or binding, of the set of atoms @{text
   "as"} in the body @{text "x"}.
 
   The first question we have to answer is when two pairs @{text "(as, x)"} and
@@ -737,7 +737,8 @@
   This lemma allows us to use our quotient package and introduce 
   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
   representing alpha-equivalence classes of pairs of type 
-  @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}. 
+  @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
+  (in the third case). 
   The elements in these types will be, respectively, written as:
 
   \begin{center}
@@ -776,7 +777,7 @@
   \noindent
   and also
   %
-  \begin{equation}
+  \begin{equation}\label{absperm}
   @{thm permute_Abs[no_vars]}
   \end{equation}
 
@@ -797,7 +798,7 @@
   \end{proof}
 
   \noindent
-  This lemma allows us to show
+  This lemma together with \eqref{absperm} allows us to show
   %
   \begin{equation}\label{halfone}
   @{thm abs_supports(1)[no_vars]}
@@ -890,7 +891,7 @@
   \end{center}
   
   \noindent
-  whereby some of the @{text ty}$'_{1..l}$ (or their components) might be contained
+  whereby some of the @{text ty}$'_{1..l}$ (or their components) can be contained
   in the collection of @{text ty}$^\alpha_{1..n}$ declared in
   \eqref{scheme}. 
   In this case we will call the corresponding argument a
@@ -941,7 +942,7 @@
   restriction we impose on shallow binders is that in case of
   \isacommand{bind\_set} and \isacommand{bind\_res} the {\it labels} must
   either refer to atom types or to sets of atom types; in case of
-  \isacommand{bind} we allow labels to atom types or lists of atom types. Two
+  \isacommand{bind} we allow labels to refer to atom types or lists of atom types. Two
   examples for the use of shallow binders are the specification of
   lambda-terms, where a single name is bound, and type-schemes, where a finite
   set of names is bound:
@@ -966,11 +967,15 @@
   \end{center}
 
   \noindent
-  Note that in this specification @{text "name"} refers to an atom type, and
-  @{text "fset"} to the type of finite sets. Shallow binders can occur in the 
-  binding part of several binding clauses. 
- 
-  A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
+  Note that for @{text lam} we have a choice which mode we use. The reason is that 
+  we bind only a single @{text name}. Having \isacommand{bind\_set} in the second
+  case changes the semantics of the specification. 
+  Note also that in these specifications @{text "name"} refers to an atom type, and
+  @{text "fset"} to the type of finite sets. 
+
+  The restrictions are as follows:
+  Shallow binders can occur in the binding part of several binding clauses. 
+  A \emph{deep} binder, on the other hand, uses an auxiliary binding function that ``picks'' out
   the atoms in one argument of the term-constructor, which can be bound in  
   other arguments and also in the same argument (we will
   call such binders \emph{recursive}, see below). 
@@ -1004,7 +1009,8 @@
   
   \noindent
   In this specification the function @{text "bn"} determines which atoms of @{text  p} are
-  bound in the argument @{text "t"}. Note that in the second-last clause the function @{text "atom"}
+  bound in the argument @{text "t"}. Note that in the second-last @{text bn}-clause the 
+  function @{text "atom"}
   coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows
   us to treat binders of different atom type uniformly.