# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1316600612 -7200
# Node ID a9e618b25656ea5289c69eba7d3cc6f075f8ef2a
# Parent  1447c135080c26170e9515a6e0b568c0ef2c0d10
some minor polishing

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