--- a/Paper/Paper.thy	Sun Apr 04 21:39:28 2010 +0200
+++ b/Paper/Paper.thy	Tue Apr 06 07:36:15 2010 +0200
@@ -1491,7 +1491,7 @@
   "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text
   "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
   "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the 
-  user, since the are given in terms of the isomorphisms we obtained by 
+  user, since they are given in terms of the isomorphisms we obtained by 
   creating new types in Isabelle/HOL (recall the picture shown in the 
   Introduction).
 
@@ -1562,7 +1562,7 @@
   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 
   Next we lift the permutation operations defined in \eqref{ceqvt} for
   the raw term-constructors @{text "C"}. These facts contain, in addition 
-  to the term-constructors, also permutations operations. In order to make the 
+  to the term-constructors, also permutation operations. In order to make the 
   lifting to go through, 
   we have to know that the permutation operations are respectful 
   w.r.t.~alpha-equivalence. This amounts to showing that the 
@@ -1576,7 +1576,7 @@
   \noindent
   for our infrastructure. In a similar fashion we can lift the equations
   characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fv_bn\<AL>\<^isub>k"}, and the 
-  binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for this
+  binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for these
   lifting are the properties:
   %
   \begin{equation}\label{fnresp}