--- a/Paper/Paper.thy	Sun May 23 16:45:00 2010 +0100
+++ b/Paper/Paper.thy	Mon May 24 22:47:06 2010 +0100
@@ -556,7 +556,7 @@
  
   \noindent
   From property \eqref{equivariancedef} and the definition of @{text supp}, we 
-  can be easily deduce that equivariant functions have empty support. There is
+  can easily deduce that equivariant functions have empty support. There is
   also a similar notion for equivariant relations, say @{text R}, namely the property
   that
   %
@@ -593,7 +593,7 @@
 
   Most properties given in this section are described in detail in \cite{HuffmanUrban10}
   and of course all are formalised in Isabelle/HOL. In the next sections we will make 
-  extensively use of these properties in order to define alpha-equivalence in 
+  extensive use of these properties in order to define alpha-equivalence in 
   the presence of multiple binders.
 *}
 
@@ -623,7 +623,7 @@
   variables; moreover there must be a permutation @{text p} such that {\it
   ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
   {\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
-  say \mbox{@{text "_ R _"}}, two equivalent terms. We also require {\it iv)} that
+  say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it iv)}
   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
   requirements {\it i)} to {\it iv)} can be stated formally as follows:
   %
@@ -638,7 +638,7 @@
   \end{equation}
 
   \noindent
-  Note that this relation is dependent on the permutation @{text
+  Note that this relation depends on the permutation @{text
   "p"}. Alpha-equivalence between two pairs is then the relation where we
   existentially quantify over this @{text "p"}. Also note that the relation is
   dependent on a free-variable function @{text "fv"} and a relation @{text
@@ -692,20 +692,20 @@
   \noindent
   Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
   \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
-  @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to $\approx_{\textit{set}}$ and
-  $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>
-  y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}
-  $\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} since there is no permutation
-  that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also
-  leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is
-  @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x, y}, x)"} which holds by 
-  taking @{text p} to be the
-  identity permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
-  $\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 abstract a single atom. 
+  @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
+  $\approx_{\textit{set}}$ and $\approx_{\textit{res}}$ by taking @{text p} to
+  be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
+  "([x, y], x \<rightarrow> y)"} $\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
+  since there is no permutation that makes the lists @{text "[x, y]"} and
+  @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
+  unchanged. Another example is @{text "({x}, x)"} $\approx_{\textit{res}}$
+  @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
+  permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
+  $\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
+  abstract a single atom.
 
   In the rest of this section we are going to introduce three abstraction 
   types. For this we define 
@@ -941,16 +941,16 @@
   of the specification (the corresponding alpha-equivalence will differ). We will 
   show this later with an example.
   
-  There are some restrictions we need to impose: First, a body can only occur
-  in \emph{one} binding clause of a term constructor. For binders we
-  distinguish between \emph{shallow} and \emph{deep} binders.  Shallow binders
-  are just labels. The restriction we need to impose on them is that in case
-  of \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either
-  refer to atom types or to sets of atom types; in case of \isacommand{bind}
-  the labels must refer to atom types 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:
+  There are some restrictions we need to impose on binding clasues: First, a
+  body can only occur in \emph{one} binding clause of a term constructor. For
+  binders we distinguish between \emph{shallow} and \emph{deep} binders.
+  Shallow binders are just labels. The restriction we need to impose on them
+  is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the
+  labels must either refer to atom types or to sets of atom types; in case of
+  \isacommand{bind} the labels must refer to atom types 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:
 
   \begin{center}
   \begin{tabular}{@ {}cc@ {}}
@@ -974,7 +974,7 @@
   \noindent
   Note that for @{text lam} it does not matter which binding mode we use. The
   reason is that we bind only a single @{text name}. However, having
-  \isacommand{bind\_set} or \isacommand{bind} in the second case makes again a
+  \isacommand{bind\_set} or \isacommand{bind} in the second case makes a
   difference to the semantics of the specification. Note also that in
   these specifications @{text "name"} refers to an atom type, and @{text
   "fset"} to the type of finite sets.