diff -r 1447c135080c -r a9e618b25656 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Sep 21 12:08:03 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 12:23:32 2011 +0200
@@ -764,7 +764,7 @@
   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 three notions of alpha-equivalence coincide, if we only
-  abstract a single atom. In this case they also agree with alpha-equivalence
+  abstract a single atom. In this case they also agree with the alpha-equivalence
   used in older versions of Nominal Isabelle \cite{Urban08}.
 
   In the rest of this section we are going to show that the alpha-equivalences