--- a/Paper/Paper.thy	Fri Jul 23 16:42:00 2010 +0200
+++ b/Paper/Paper.thy	Fri Jul 23 16:42:47 2010 +0200
@@ -372,7 +372,7 @@
   about them in a theorem prover would be a major pain.  \medskip
 
   \noindent
-  {\bf Contributions:}  We provide three novel definitions for when terms
+  {\bf Contributions:}  We provide three new definitions for when terms
   involving general binders are $\alpha$-equivalent. These definitions are
   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
   proofs, we establish a reasoning infrastructure for $\alpha$-equated
@@ -551,8 +551,8 @@
 
   \begin{property}\label{supportsprop}
   Given a set @{text "as"} of atoms.
-  {\it i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
-  {\it ii)} @{thm supp_supports[no_vars]}.
+  {\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
+  {\it (ii)} @{thm supp_supports[no_vars]}.
   \end{property}
 
   Another important notion in the nominal logic work is \emph{equivariance}.
@@ -1468,8 +1468,7 @@
   involving multiple binders. As above, we first build the tuples @{text "D"} and
   @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
   compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). 
-  For $\approx_{\,\textit{set}}$ (respectively $\approx_{\,\textit{list}}$ and 
-  $\approx_{\,\textit{res}}$)  we also need
+  For $\approx_{\,\textit{set}}$  we also need
   a compound free-atom function for the bodies defined as
   %
   \begin{center}
@@ -1477,7 +1476,7 @@
   \end{center}
 
   \noindent
-  with assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$.
+  with the assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$.
   The last ingredient we need are the sets of atoms bound in the bodies.
   For this we take
 
@@ -2179,7 +2178,7 @@
 text {*
   We have presented an extension of Nominal Isabelle for dealing with
   general binders, that is term-constructors having multiple bound 
-  variables. For this extension we introduced novel definitions of 
+  variables. For this extension we introduced new definitions of 
   $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
   To specify general binders we used the specifications from Ott, but extended them 
   in some places and restricted