--- a/LMCS-Paper/Paper.thy	Sun Sep 18 19:38:19 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Sun Sep 18 22:52:56 2011 +0200
@@ -304,8 +304,8 @@
   \draw (-2.0, 0.845) --  (0.7,0.845);
   \draw (-2.0,-0.045)  -- (0.7,-0.045);
 
-  \draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
-  \draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
+  \draw ( 0.7, 0.5) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};
+  \draw (-2.4, 0.5) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
   \draw (1.8, 0.48) node[right=-0.1mm]
     {\small\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
   \draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
@@ -661,7 +661,7 @@
 
   In order to keep our work with deriving the reasoning infrastructure
   manageable, we will wherever possible state definitions and perform proofs
-  on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that
+  on the ``user-level'' of Isabelle/HOL, as opposed to writing custom ML-code that
   generates them anew for each specification. 
   To that end, we will consider
   first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs
@@ -1284,7 +1284,7 @@
   But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
   that a notion is given for alpha-equivalence classes and leave it out 
   for the corresponding notion given on the ``raw'' level. So for example 
-  we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}
+  we have @{text "ty\<^sup>\<alpha> / ty"} and @{text "C\<^sup>\<alpha> / C"}
   where @{term ty} is the type used in the quotient construction for 
   @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the ``raw'' type @{text "ty"},
   respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor of @{text "ty\<^sup>\<alpha>"}. 
@@ -2594,8 +2594,6 @@
 section {* Conclusion *}
 
 text {*
-  %%Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure).
-
 
   We have presented an extension of Nominal Isabelle for dealing with general
   binders, that is term-constructors having multiple bound variables. For this
@@ -2653,7 +2651,8 @@
   informal notes \cite{SewellBestiary} available to us and also for patiently
   explaining some of the finer points of the Ott-tool.  Stephanie Weirich
   suggested to separate the subgrammars of kinds and types in our Core-Haskell
-  example.
+  example. Ramana Kumar helped us with comments about an earlier version of 
+  this paper.
 *}