# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269949055 -7200
# Node ID 8c59c8a0721cef9e817c79994fd3ff237149b78f
# Parent  a3f923d88215a0e4a839c1743fac3d0ba4588be5
merged

diff -r a3f923d88215 -r 8c59c8a0721c Paper/Paper.thy
--- 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.
 *}