--- a/Paper/Paper.thy	Tue Mar 30 13:36:02 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 13:37:35 2010 +0200
@@ -573,10 +573,9 @@
   in @{text x}, because @{term "p \<bullet> x = x"}.
 
   All properties given in this section are formalised in Isabelle/HOL and also
-  most of them are described with proofs in \cite{HuffmanUrban10}. In the next section 
-  we make extensively use of the properties of @{text "supp"} and permutations 
-  for characterising alpha-equivalence in the presence of multiple binders.
- 
+  most of them are described with proofs in \cite{HuffmanUrban10}. In the next
+  sections we will make extensively use of these properties for characterising
+  alpha-equivalence in the presence of multiple binders.
 *}