--- a/Paper/Paper.thy	Tue May 18 11:47:29 2010 +0200
+++ b/Paper/Paper.thy	Tue May 18 14:40:05 2010 +0100
@@ -922,30 +922,33 @@
   ``\isacommand{bind}-part'' will be called \emph{binders}. 
 
   In contrast to Ott, we allow multiple labels in binders and bodies. For example
-  we have binding clauses of the form:
+  we allow binding clauses of the form:
 
   \begin{center}
-  \begin{tabular}{ll}
-  @{text "Foo x::name y::name t::lam s::lam"} &  
-      \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}  
+  \begin{tabular}{@ {}ll@ {}}
+  @{text "Foo\<^isub>1 x::name y::name t::lam s::lam"} &  
+      \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
+  @{text "Foo\<^isub>2 x::name y::name t::lam s::lam"} &  
+      \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, 
+      \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
   \end{tabular}
   \end{center}
 
   \noindent
-  Similarly for the other binding modes.
+  Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}
+  and \isacommand{bind\_res} the binding clauses will make a difference in
+  terms of the corresponding alpha-equivalence. We will show this later with an example.
   
-
-  There are a few restrictions we need to impose: First, a body can only occur in
-  \emph{one} binding clause of a term constructor. 
-  For binders we distinguish between \emph{shallow} and \emph{deep} binders.
-  Shallow binders are just labels. The
-  restriction we need to impose on them is that in case of
-  \isacommand{bind\_set} and \isacommand{bind\_res} the labels must
-  either refer to atom types or to sets of atom types; in case of
-  \isacommand{bind} the labels must 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:
+  There are some restrictions we need to impose: First, a body can only occur
+  in \emph{one} binding clause of a term constructor. For binders we
+  distinguish between \emph{shallow} and \emph{deep} binders.  Shallow binders
+  are just labels. The restriction we need to impose on them is that in case
+  of \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either
+  refer to atom types or to sets of atom types; in case of \isacommand{bind}
+  the labels must 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:
 
   \begin{center}
   \begin{tabular}{@ {}cc@ {}}
@@ -967,23 +970,25 @@
   \end{center}
 
   \noindent
-  Note that for @{text lam} it does not matter which binding mode we use. The reason is that 
-  we bind only a single @{text name}. However, having \isacommand{bind\_set} or 
-  \isacommand{bind} 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. 
+  Note that for @{text lam} it does not matter which binding mode we use. The
+  reason is that we bind only a single @{text name}. However, having
+  \isacommand{bind\_set} or \isacommand{bind} in the second case again makes a
+  difference to the underlying notion of alpha-equivalence. Note also that in
+  these specifications @{text "name"} refers to an atom type, and @{text
+  "fset"} to the type of finite sets.
+
 
   A \emph{deep} binder 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). 
-  The corresponding binding functions are expected to return either a set of atoms
-  (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms
-  (for \isacommand{bind}). They can be defined by primitive recursion over the
-  corresponding type; the equations must be given in the binding function part of
-  the scheme shown in \eqref{scheme}. For example a term-calculus containing @{text "Let"}s 
-  with tuple patterns might be specified as:
+  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). The corresponding binding functions are
+  expected to return either a set of atoms (for \isacommand{bind\_set} and
+  \isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can
+  be defined by primitive recursion over the corresponding type; the equations
+  must be given in the binding function part of the scheme shown in
+  \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
+  tuple patterns might be specified as:
+
   %
   \begin{equation}\label{letpat}
   \mbox{%
@@ -1065,9 +1070,7 @@
 
   \noindent
   The reason why we must exclude such specifications is that they cannot be
-  represented by the general binders described in Section
-  \ref{sec:binders}. Unlike shallow binders, we restrict deep binders to occur
-  in only one binding clause.
+  represented by the general binders described in Section~\ref{sec:binders}. 
 
   We also need to restrict the form of the binding functions. As will shortly
   become clear, we cannot return an atom in a binding function that is also
@@ -1084,7 +1087,7 @@
   (case @{text PTup}). This restriction will simplify some automatic proofs
   later on.
   
-  In order to simplify later definitions, we shall assume specifications 
+  In order to simplify our definitions, we shall assume specifications 
   of term-calculi are \emph{completed}. By this we mean that  
   for every argument of a term-constructor that is \emph{not} 
   already part of a binding clause, we add implicitly a special \emph{empty} binding