# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1316611112 -7200
# Node ID af6eda1fb91fefc067228a637e74280e2ac6ab86
# Parent  a9e618b25656ea5289c69eba7d3cc6f075f8ef2a
added a footnote

diff -r a9e618b25656 -r af6eda1fb91f LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Sep 21 12:23:32 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 15:18:32 2011 +0200
@@ -765,7 +765,9 @@
   (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 the alpha-equivalence
-  used in older versions of Nominal Isabelle \cite{Urban08}.
+  used in older versions of Nominal Isabelle \cite{Urban08}.\footnote{We omit a
+  proof of this fact since the details are hairy and not really important for the
+  purpose of this paper.}
 
   In the rest of this section we are going to show that the alpha-equivalences
   really lead to abstractions where some atoms are bound (or more precisely