--- a/Paper/Paper.thy	Wed Apr 21 16:25:24 2010 +0200
+++ b/Paper/Paper.thy	Wed Apr 21 17:42:57 2010 +0200
@@ -338,7 +338,7 @@
   (Note that this means also the term-constructors for variables, applications
   and lambda are lifted to the quotient level.)  This construction, of course,
   only works if alpha-equivalence is indeed an equivalence relation, and the
-  lifted definitions and theorems are respectful w.r.t.~alpha-equivalence.
+  ``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence.
   For example, we will not be able to lift a bound-variable function. Although
   this function can be defined for raw terms, it does not respect
   alpha-equivalence and therefore cannot be lifted. To sum up, every lifting
@@ -352,7 +352,7 @@
   known as Core-Haskell (see Figure~\ref{corehas}). This term language
   involves patterns that have lists of type-, coercion- and term-variables,
   all of which are bound in @{text "\<CASE>"}-expressions. One
-  difficulty is that we do not know in advance how many variables need to
+  feature is that we do not know in advance how many variables need to
   be bound. Another is that each bound variable comes with a kind or type
   annotation. Representing such binders with single binders and reasoning
   about them in a theorem prover would be a major pain.  \medskip
@@ -932,9 +932,9 @@
 
   \begin{center}
   \begin{tabular}{l}
-  \isacommand{bind}\; {\it binder}\; \isacommand{in}\; {\it label}\\
-  \isacommand{bind\_set}\; {\it binder}\; \isacommand{in}\; {\it label}\\
-  \isacommand{bind\_res}\; {\it binder}\; \isacommand{in}\; {\it label}\\
+  \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+  \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+  \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
   \end{tabular}
   \end{center}
 
@@ -943,15 +943,15 @@
   the second is for sets of binders (the order does not matter, but the
   cardinality does) and the last is for sets of binders (with vacuous binders
   preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding
-  clause will be called the \emph{body}; the ``\isacommand{bind}-part'' will
-  be called the \emph{binder}.
+  clause will be called \emph{body}; the ``\isacommand{bind}-part'' will
+  be called \emph{binder}.
 
   In addition we distinguish between \emph{shallow} and \emph{deep}
-  binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;
-  \isacommand{in}\; {\it label'} (similar for the other two modes). The
-  restriction we impose on shallow binders is that the {\it label} must either
-  refer to a type that is an atom type or to a type that is a finite set or
-  list of an atom type. Two examples for the use of shallow binders are the
+  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 the {\it labels} must either
+  refer to atom types or to finite sets 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:
 
@@ -1111,8 +1111,9 @@
  
   Having dealt with all syntax matters, the problem now is how we can turn
   specifications into actual type definitions in Isabelle/HOL and then
-  establish a reasoning infrastructure for them. Because of the problem
-  Pottier and Cheney pointed out, we cannot in general re-arrange arguments of
+  establish a reasoning infrastructure for them. As
+  Pottier and Cheney pointed out \cite{Pottier06,Cheney5}, we cannot in general 
+  re-arrange arguments of
   term-constructors so that binders and their bodies are next to each other, and
   then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
   @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first