--- a/Paper/Paper.thy	Fri Oct 01 07:11:47 2010 -0400
+++ b/Paper/Paper.thy	Mon Oct 04 07:25:37 2010 +0100
@@ -546,10 +546,10 @@
   such approximations can be simplified with the notion \emph{supports}, defined 
   as follows:
 
-  \begin{defn}
+  \begin{definition}
   A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
   not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
-  \end{defn}
+  \end{definition}
 
   \noindent
   The main point of @{text supports} is that we can establish the following 
@@ -779,7 +779,7 @@
   \emph{abstractions}. The important property we need to derive is the support of 
   abstractions, namely:
 
-  \begin{thm}[Support of Abstractions]\label{suppabs} 
+  \begin{theorem}[Support of Abstractions]\label{suppabs} 
   Assuming @{text x} has finite support, then\\[-6mm] 
   \begin{center}
   \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -788,7 +788,7 @@
   @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}
   \end{tabular}
   \end{center}
-  \end{thm}
+  \end{theorem}
 
   \noindent
   Below we will show the first equation. The others 
@@ -2088,7 +2088,7 @@
   Two formalisations involving general binders have been 
   performed in older
   versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W 
-  \cite{BengtsonParow09, UrbanNipkow09}).  Both
+  \cite{BengtsonParow09,UrbanNipkow09}).  Both
   use the approach based on iterated single binders. Our experience with
   the latter formalisation has been disappointing. The major pain arose from
   the need to ``unbind'' variables. This can be done in one step with our