--- a/LMCS-Paper/Paper.thy	Thu Dec 29 18:05:13 2011 +0000
+++ b/LMCS-Paper/Paper.thy	Mon Jan 09 10:12:46 2012 +0000
@@ -188,7 +188,7 @@
 
   \noindent
   As a result, we provide three general binding mechanisms each of which binds
-  multiple variables at once, and let the user chose which one is intended
+  multiple variables at once, and let the user choose which one is intended
   when formalising a term-calculus.
 
   By providing these general binding mechanisms, however, we have to work
@@ -449,7 +449,7 @@
 section {* A Short Review of the Nominal Logic Work *}
 
 text {*
-  At its core, Nominal Isabelle is an adaption of the nominal logic work by
+  At its core, Nominal Isabelle is an adaptation of the nominal logic work by
   Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
   \cite{HuffmanUrban10} (including proofs). We shall briefly review this work
   to aid the description of what follows. 
@@ -783,7 +783,7 @@
   \end{equation}\smallskip
   
   \noindent
-  Note that in these relation we replaced the free-atom function @{text "fa"}
+  Note that in these relations we replaced the free-atom function @{text "fa"}
   with @{term "supp"} and the relation @{text R} with equality. We can show
   the following two properties:
 
@@ -958,7 +958,7 @@
   datatype package of Isabelle/HOL \cite{Berghofer99} 
   and by the syntax of the
   Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
-  collection of (possibly mutual recursive) type declarations, say @{text
+  collection of (possibly mutually recursive) type declarations, say @{text
   "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
   binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
   syntax in Nominal Isabelle for such specifications is schematically as follows:
@@ -1889,7 +1889,7 @@
   \]\smallskip
   
   \noindent
-  We call these conditions as \emph{quasi-injectivity}. They correspond to the
+  We call these conditions \emph{quasi-injectivity}. They correspond to the
   premises in our alpha-equiva\-lence relations, except that the
   relations @{text "\<approx>ty"}$_{1..n}$ are all replaced by equality (and similarly
   the free-atom and binding functions are replaced by their lifted
@@ -1943,7 +1943,7 @@
   \noindent
   whereby the @{text P}$_{1..n}$ are the properties established by the
   induction, and the @{text y}$_{1..n}$ are of type @{text
-  "ty\<AL>"}$_{1..n}$. Note that for the term constructors @{text
+  "ty\<AL>"}$_{1..n}$. Note that for the term constructor @{text
   "C"}$^\alpha_1$ the induction principle has a hypothesis of the form
 
   \[
@@ -2207,7 +2207,7 @@
   \noindent
   They are stronger in the sense that they allow us to assume in the @{text
   "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms
-  avoid, or being fresh for, a context @{text "c"} (which is assumed to be finitely supported).
+  avoid, or are fresh for, a context @{text "c"} (which is assumed to be finitely supported).
   
   These stronger cases lemmas can be derived from the `weak' cases lemmas
   given in \eqref{inductex}. This is trivial in case of patterns (the one on