--- a/Paper/Paper.thy	Fri May 14 21:18:34 2010 +0100
+++ b/Paper/Paper.thy	Sat May 15 22:06:06 2010 +0100
@@ -253,7 +253,7 @@
 
   Our insistence on reasoning with alpha-equated terms comes from the
   wealth of experience we gained with the older version of Nominal Isabelle:
-  for non-trivial properties, reasoning about alpha-equated terms is much
+  for non-trivial properties, reasoning with alpha-equated terms is much
   easier than reasoning with raw terms. The fundamental reason for this is
   that the HOL-logic underlying Nominal Isabelle allows us to replace
   ``equals-by-equals''. In contrast, replacing
@@ -295,7 +295,7 @@
   \noindent
   We take as the starting point a definition of raw terms (defined as a
   datatype in Isabelle/HOL); identify then the alpha-equivalence classes in
-  the type of sets of raw terms according to our alpha-equivalence relation
+  the type of sets of raw terms according to our alpha-equivalence relation,
   and finally define the new type as these alpha-equivalence classes
   (non-emptiness is satisfied whenever the raw terms are definable as datatype
   in Isabelle/HOL and the property that our relation for alpha-equivalence is
@@ -495,8 +495,8 @@
   @{thm (rhs) fresh_star_def[no_vars]}.
   A striking consequence of these definitions is that we can prove
   without knowing anything about the structure of @{term x} that
-  swapping two fresh atoms, say @{text a} and @{text b}, leave 
-  @{text x} unchanged. 
+  swapping two fresh atoms, say @{text a} and @{text b}, leaves 
+  @{text x} unchanged:
 
   \begin{property}\label{swapfreshfresh}
   @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
@@ -933,12 +933,13 @@
 
   \noindent
   Similarly for the other binding modes.
+  
+
   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
-  restrictions we need to impose on them are that in case of
+  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. 
@@ -967,8 +968,8 @@
 
   \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 even 
-  \isacommand{bind}, in the second
+  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. 
@@ -1006,63 +1007,26 @@
   \end{equation}
   
   \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 @{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. 
+  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 @{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.
 
-  The most drastic restriction we have to impose on deep binders is that 
-  we cannot have more than one binding function for one binder. Consider for example the 
-  term-constructors:
-
+  As said above, for deep binders we allow binding clauses such as
+  %
   \begin{center}
   \begin{tabular}{ll}
-  @{text "Foo\<^isub>1 p::pat t::trm"} & 
-     \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
-  @{text "Foo\<^isub>2 x::name p::pat t::trm"} & 
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}, ***\\ 
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t}
-  and also all atoms from @{text q} in @{text t}. Unfortunately, we have no way
-  to determine whether the binder came from the binding function @{text
-  "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why
-  we must exclude such specifications is that they cannot be represented by
-  the general binders described in Section \ref{sec:binders}. However
-  the following two term-constructors are allowed
-
-  \begin{center}
-  \begin{tabular}{ll}
-  @{text "Bar\<^isub>1 p::pat t::trm s::trm"} & 
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t s"}\\
-  @{text "Bar\<^isub>2 p::pat t::trm"} &  
+  @{text "Bar p::pat t::trm"} &  
      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\
   \end{tabular}
   \end{center}
 
   \noindent
-  since there is no overlap of binders. Unlike shallow binders, we restrict deep
-  binders to occur in only one binding clause. Therefore @{text "Bar\<^isub>2"} cannot 
-  be reformulated as
-
-  \begin{center}
-  \begin{tabular}{ll}
-  @{text "Bar\<^isub>3 p::pat t::trm"} &  
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p"}, 
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t"}\\
-  \end{tabular}
-  \end{center}
-  
-  Note that in the @{text "Bar\<^isub>2"}, we wrote \isacommand{bind}~@{text
-  "bn(p)"}~\isacommand{in}~@{text "p.."}.  Whenever such a binding clause 
-  is present, where the argument in the binder also occurs in the body, we will 
-  call the corresponding binder \emph{recursive}.  To see the
-  purpose of such recursive binders, compare ``plain'' @{text "Let"}s and
-  @{text "Let_rec"}s in the following specification:
+  where the argument of the deep binder is also in the body. We call such
+  binders \emph{recursive}.  To see the purpose of such recursive binders,
+  compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
+  specification:
   %
   \begin{equation}\label{letrecs}
   \mbox{%
@@ -1088,6 +1052,22 @@
   inside the assignment. This difference has consequences for the free-variable 
   function and alpha-equivalence relation, which we are going to describe in the 
   rest of this section.
+  
+  The restriction we have to impose on deep binders is that we cannot have
+  more than one binding function for one binder. So we exclude:
+
+  \begin{center}
+  \begin{tabular}{ll}
+  @{text "Baz p::pat t::trm"} & 
+     \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
+  \end{tabular}
+  \end{center}
+
+  \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.
 
   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
@@ -1104,7 +1084,7 @@
   (case @{text PTup}). This restriction will simplify some automatic proofs
   later on.
   
-  In order to simplify some later definitions, we shall assume specifications 
+  In order to simplify later 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