--- a/Paper/Paper.thy	Mon May 24 22:47:06 2010 +0100
+++ b/Paper/Paper.thy	Tue May 25 07:59:16 2010 +0200
@@ -85,7 +85,7 @@
   also there one would like to bind multiple variables at once.
 
   Binding multiple variables has interesting properties that cannot be captured
-  easily by iterating single binders. For example in case of type-schemes we do not
+  easily by iterating single binders. For example in the case of type-schemes we do not
   want to make a distinction about the order of the bound variables. Therefore
   we would like to regard the following two type-schemes as alpha-equivalent
   %
@@ -183,10 +183,10 @@
   where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"}
   becomes bound in @{text s}. In this representation the term 
   \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
-  instance, but the lengths of two lists do not agree. To exclude such terms, 
+  instance, but the lengths of the two lists do not agree. To exclude such terms, 
   additional predicates about well-formed
   terms are needed in order to ensure that the two lists are of equal
-  length. This can result into very messy reasoning (see for
+  length. This can result in very messy reasoning (see for
   example~\cite{BengtsonParow09}). To avoid this, we will allow type
   specifications for $\mathtt{let}$s as follows
   %
@@ -220,7 +220,7 @@
   inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 
   However, we will not be able to cope with all specifications that are
-  allowed by Ott. One reason is that Ott lets the user to specify ``empty'' 
+  allowed by Ott. One reason is that Ott lets the user specify ``empty'' 
   types like
 
   \begin{center}
@@ -704,7 +704,7 @@
   $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no
   permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
   (similarly for $\approx_{\textit{list}}$).  It can also relatively easily be
-  shown that all tree notions of alpha-equivalence coincide, if we only
+  shown that all three notions of alpha-equivalence coincide, if we only
   abstract a single atom.
 
   In the rest of this section we are going to introduce three abstraction 
@@ -1119,7 +1119,7 @@
   term-constructors so that binders and their bodies are next to each other will 
   result in inadequate representations. Therefore we will first
   extract datatype definitions from the specification and then define 
-  expicitly an alpha-equivalence relation over them.
+  explicitly an alpha-equivalence relation over them.
 
 
   The datatype definition can be obtained by stripping off the 
@@ -1152,7 +1152,7 @@
   @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
   \end{equation}
   
-  The first non-trivial step we have to perform is the generation free-variable 
+  The first non-trivial step we have to perform is the generation of free-variable 
   functions from the specifications. For atomic types we define the auxilary
   free variable functions:
 
@@ -1455,7 +1455,7 @@
 
   \begin{proof} 
   The proof is by mutual induction over the definitions. The non-trivial
-  cases involve premises build up by $\approx_{\textit{set}}$, 
+  cases involve premises built up by $\approx_{\textit{set}}$, 
   $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They 
   can be dealt with as in Lemma~\ref{alphaeq}.
   \end{proof}
@@ -1526,7 +1526,7 @@
   \end{center} 
 
   \noindent
-  for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties
+  for all @{text "y\<^isub>i"} whereby 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
@@ -1540,7 +1540,7 @@
   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 permutation operations. In order to make the 
-  lifting to go through, 
+  lifting go through, 
   we have to know that the permutation operations are respectful 
   w.r.t.~alpha-equivalence. This amounts to showing that the 
   alpha-equivalence relations are equivariant, which we already established 
@@ -1567,7 +1567,7 @@
 
   \noindent
   which can be established by induction on @{text "\<approx>ty"}. Whereas the first
-  property is always true by the way how we defined the free-variable
+  property is always true by the way we defined the free-variable
   functions for types, the second and third do \emph{not} hold in general. There is, in principle, 
   the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound
   variable. Then the third property is just not true. However, our 
@@ -1864,7 +1864,7 @@
   \end{center}
 
   \noindent
-  So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we are can equally
+  So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
   establish
 
   \begin{center}
@@ -1894,7 +1894,7 @@
   we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
   This completes the proof showing that the strong induction principle derives from
   the weak induction principle. For the moment we can derive the difficult cases of 
-  the strong induction principles only by hand, but they are very schematically 
+  the strong induction principles only by hand, but they are very schematic 
   so that with little effort we can even derive them for 
   Core-Haskell given in Figure~\ref{nominalcorehas}. 
 *}