--- a/Paper/Paper.thy	Sat Mar 20 18:16:26 2010 +0100
+++ b/Paper/Paper.thy	Sun Mar 21 22:27:08 2010 +0100
@@ -44,7 +44,7 @@
   \end{center}
 
   \noindent
-  and the quantification binds at once a finite (possibly empty) set of
+  and the quantification $\forall$ binds a finite (possibly empty) set of
   type-variables.  While it is possible to implement this kind of more general
   binders by iterating single binders, this leads to a rather clumsy
   formalisation of W. The need of iterating single binders is also one reason
@@ -86,7 +86,7 @@
   definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
 
   However, the notion of alpha-equivalence that is preserved by vacuous binders is not
-  alway wanted. For example in terms like
+  always wanted. For example in terms like
 
   \begin{equation}\label{one}
   \LET x = 3 \AND y = 2 \IN x\,-\,y \END
@@ -117,7 +117,7 @@
   \noindent
   we want to bind all variables from the pattern inside the body of the
   $\mathtt{let}$, but we also care about the order of these variables, since
-  we do not want to identify \eqref{two} with
+  we do not want to regard \eqref{two} as alpha-equivalent with
 
   \begin{center}
   $\LET (y, x) = (3, 2) \IN x\,- y\,\END$
@@ -125,7 +125,7 @@
 
   \noindent
   As a result, we provide three general binding mechanisms each of which binds multiple
-  variables at once, and we let the user chose which one is intended when formalising a
+  variables at once, and let the user chose which one is intended when formalising a
   programming language calculus.
 
   By providing these general binding mechanisms, however, we have to work around 
@@ -147,13 +147,13 @@
   \end{center}
 
   \noindent
-  where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become 
-  bound in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$}
-  would be perfectly legal instance, and so one needs additional predicates about terms 
-  to ensure that the two lists are of equal length. This can result into very 
-  messy reasoning (see for example~\cite{BengtsonParow09}). 
-  To avoid this, we will allowto specify for example $\mathtt{let}$s 
-  as follows
+  where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound
+  in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$}
+  would be a perfectly legal instance. To exclude such terms an additional
+  predicate about well-formed terms is needed in order to ensure that the two
+  lists are of equal length. This can result into very messy reasoning (see
+  for example~\cite{BengtsonParow09}). To avoid this, we will allow specifications
+  for $\mathtt{let}$s as follows
 
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
@@ -167,7 +167,7 @@
   \noindent
   where $assn$ is an auxiliary type representing a list of assignments
   and $bn$ an auxiliary function identifying the variables to be bound by 
-  the $\mathtt{let}$. This function can be defined by recursion over $assn$ as 
+  the $\mathtt{let}$. This function is defined by recursion over $assn$ as follows
 
   \begin{center}
   $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$