--- a/LMCS-Paper/Paper.thy	Wed Sep 21 15:18:32 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 18:27:24 2011 +0200
@@ -2177,7 +2177,7 @@
   principle. Once these two proof obligations are discharged, the reasoning
   infrastructure of the function package will automatically derive the
   stronger induction principle. This way of establishing the stronger induction
-  principle is considerably simpler than the earlier work presented \cite{Urban08}.
+  principle is considerably simpler than the earlier work presented in \cite{Urban08}.
 
   As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,
   which we lifted in the previous section and which are all well-founded. It
@@ -2207,7 +2207,7 @@
   \noindent
   They are stronger in the sense that they allow us to assume in the @{text
   "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms
-  avoid a context @{text "c"} (which is assumed to be finitely supported).
+  avoid, or being fresh for, a context @{text "c"} (which is assumed to be finitely supported).
   
   These stronger cases lemmas can be derived from the `weak' cases lemmas
   given in \eqref{inductex}. This is trivial in case of patterns (the one on
@@ -2234,7 +2234,7 @@
   which we must use in order to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
   use this implication directly, because we have no information whether or not @{text
   "x\<^isub>1"} is fresh for @{text "c"}.  However, we can use Properties
-  \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: we know
+  \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}. We know
   by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\<alpha>
   x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 -
   {atom x\<^isub>1}"}). Property \ref{avoiding} provides us then with a
@@ -2310,7 +2310,7 @@
   that @{text "\<pi>"} only renames atoms that become bound. In this way @{text "\<pi>"}
   does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"} (which only tracks alpha-equivalence of terms that are not
   under the binder). However, the problem is that the
-  permutation operation @{text "\<pi> \<bullet> x\<^isub>1"} applies to all attoms in @{text "x\<^isub>1"}. To avoid this
+  permutation operation @{text "\<pi> \<bullet> x\<^isub>1"} applies to all atoms in @{text "x\<^isub>1"}. To avoid this
   we introduce an auxiliary permutation operations, written @{text "_
   \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or
   more precisely the atoms specified by the @{text "bn"}-functions) and leaves
@@ -2336,7 +2336,7 @@
   \noindent
   Using again the quotient package  we can lift the auxiliary permutation operations
   @{text "_ \<bullet>\<^bsub>bn\<^esub> _"}
-  alpha-equated terms. Moreover we can prove the following two properties
+  to alpha-equated terms. Moreover we can prove the following two properties
 
   \begin{lem}\label{permutebn} 
   Given a binding function @{text "bn\<^sup>\<alpha>"} and auxiliary equivalence @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"} 
@@ -2355,7 +2355,7 @@
   is equivalent to first permuting the binders and then calculating the bound
   atoms. The second states that @{text "_ \<bullet>\<AL>\<^bsub>bn\<^esub> _"} preserves
   @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}.  The main point of the auxiliary
-  permutation functions is that they allow us to rename just the binders in a
+  permutation functions is that they allow us to rename just the bound atoms in a
   term, without changing anything else.
   
   Having the auxiliary permutation function in place, we can now solve all remaining cases. 
@@ -2654,7 +2654,7 @@
   imagine that there is need for a binding mode where instead of usual lists,
   we abstract lists of distinct elements (the corresponding type @{text
   "dlist"} already exists in the library of Isabelle/HOL). We expect the
-  presented work can be easily extended to accommodate such binding modes.\medskip
+  presented work can be extended to accommodate such binding modes.\medskip
   
   \noindent
   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many

--- a/LMCS-Paper/document/root.bib	Wed Sep 21 15:18:32 2011 +0200
+++ b/LMCS-Paper/document/root.bib	Wed Sep 21 18:27:24 2011 +0200
@@ -1,8 +1,8 @@
 @inproceedings{pfenningsystem,
-  author =       "Frank Pfenning and Carsten Sch{\"u}rmann", 
-  title =        "System Description: Twelf---{A} Meta-Logical
-                  Framework for Deductive Systems",
-  booktitle =    "Automated Deduction",
+  author =       "F.~Pfenning and C.~Sch{\"u}rmann", 
+  title =        "{S}ystem {D}escription: {T}welf - {A} {M}eta-{L}ogical
+                  {F}ramework for {D}eductive {S}ystems",
+  booktitle =    "Proc.~of the 16th International Conference on Automated Deduction (CADE)",
   series =       "LNAI",
   volume =       1632,
   pages =        "202--206",
@@ -38,8 +38,8 @@
 
 @InProceedings{UrbanKaliszyk11,
   author =       {C.~Urban and C.~Kaliszyk},
-  title =        {General Bindings and Alpha-Equivalence in Nominal Isabelle},
-  booktitle =    {Proceedings of the 20th European Symposium on Programming (ESOP)},
+  title =        {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle},
+  booktitle =    {Proc.~of the 20th European Symposium on Programming (ESOP)},
   pages =        {480-500},
   year =         {2011},
   volume =       {6602},
@@ -50,14 +50,14 @@
 @inproceedings{KaliszykUrban11,
   author = 	 {C.~Kaliszyk and C.~Urban},
   title = 	 {{Q}uotients {R}evisited for {I}sabelle/{HOL}},
-  booktitle = 	 {Proc.~of the 26th ACM Symposium On Applied Computing (SAC)},
+  booktitle = 	 {Proc.~of the 26th ACM Symposium on Applied Computing (SAC)},
   year = 	 {2011},
   pages =        {1639--1644}
 }
 
 @InProceedings{cheney05a,
   author = 	 {J.~Cheney},
-  title = 	 {{S}crap your {N}ameplate ({F}unctional {P}earl)},
+  title = 	 {{S}crap {Y}our {N}ameplate ({F}unctional {P}earl)},
   booktitle = 	 {Proc.~of the 10th International Conference on Functional Programming (ICFP)},
   pages = 	 {180--191},
   year = 	 {2005}
@@ -137,7 +137,7 @@
 
 @inproceedings{cheney05,
   author    = {J.~Cheney},
-  title     = {{T}oward a {G}eneral {T}heory of {N}ames: {B}inding and {S}cope},
+  title     = {{T}owards a {G}eneral {T}heory of {N}ames: {B}inding and {S}cope},
   booktitle = {Proc.~of the 3rd ACM Workshop on Mechanized Reasoning about Languages 
                with Variable Binding and Names (MERLIN)},
   year      = {2005},
@@ -191,7 +191,7 @@
   author = {F.~Pottier},
   title = {{A}n {O}verview of {C$\alpha$ml}},
   year = {2006},
-  booktitle = {ACM Workshop on ML},
+  booktitle = {Proc.~of the ACM Workshop on ML},
   pages = {27--52},
   volume = {148},
   number = {2},