--- a/Paper/Paper.thy	Fri May 14 15:37:23 2010 +0200
+++ b/Paper/Paper.thy	Fri May 14 15:21:05 2010 +0100
@@ -939,11 +939,11 @@
   For binders we distinguish between \emph{shallow} and \emph{deep} binders.
   Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
   \isacommand{in}\; {\it labels'} (similar for the other two modes). The
-  restriction we impose on shallow binders is that in case of
+  restrictions we impose on shallow binders are 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 refer to atom types or lists of atom types. Two
-  examples for the use of shallow binders are the specification of
+  \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:
 
@@ -967,15 +967,14 @@
   \end{center}
 
   \noindent
-  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
+  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
   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
+  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). 
@@ -1011,11 +1010,12 @@
   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
+  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 ``overlapping'' deep binders. Consider for example the 
+  we cannot have more than one binding function for one binder. Consider for example the 
   term-constructors:
 
   \begin{center}
@@ -1540,17 +1540,17 @@
   induction principles that establish
 
   \begin{center}
-  @{text "P\<^bsub>ty\<AL>\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^isub>n\<^esub> y\<^isub>n "}
+  @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>1 y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^esub>\<^isub>n y\<^isub>n "}
   \end{center} 
 
   \noindent
-  for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^isub>i\<^esub>"} stand for properties
+  for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties
   defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of 
   these induction principles look
   as follows
 
   \begin{center}
-  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<AL>\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<AL>\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<AL>\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} 
+  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<AL>\<^esub>\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<AL>\<^esub>\<^isub>j x\<^isub>j \<Rightarrow> P\<^bsub>ty\<AL>\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} 
   \end{center}
 
   \noindent
@@ -1796,8 +1796,8 @@
 
   \begin{lemma}\label{permutebn} 
   Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
-  {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"} and {\it ii)}
-    @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"}.
+  {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"} and {\it ii)}
+    @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
   \end{lemma}
 
   \begin{proof} 
@@ -1819,7 +1819,7 @@
   \begin{equation}\label{renaming}
   \begin{array}{l}
   \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\ 
-  \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
+  \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<^bsub>bnpat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
   \end{array}
   \end{equation}