# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1279183205 -3600
# Node ID 99134763d03e2f14bf68827daebab747d21a4bb7
# Parent  46f753eeb0b8ba3d457b5f1d6e1a7b38b256bfea
a bit more to the paper

diff -r 46f753eeb0b8 -r 99134763d03e Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Jul 14 21:30:52 2010 +0100
+++ b/Paper/Paper.thy	Thu Jul 15 09:40:05 2010 +0100
@@ -1354,8 +1354,8 @@
   Recall that @{text ANil} and @{text "ACons"} have no
   binding clause in the specification. The corresponding free-atom
   function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms
-  occurring in an assignment (in case of @{text "ACons"}, they are given by 
-  calls to @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). 
+  occurring in an assignment (in case of @{text "ACons"}, they are given in
+  terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). 
   The binding only takes place in @{text Let} and
   @{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies
   that all atoms given by @{text "set (bn as)"} have to be bound in @{text
@@ -1592,7 +1592,7 @@
   in the clause for @{text "Let"} (which is has
   a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant 
   to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, 
-  because there everything from the assignment is under the binder. 
+  because there all components of an assignment are ``under'' the binder. 
 *}
 
 section {* Establishing the Reasoning Infrastructure *}
@@ -2064,8 +2064,8 @@
   To our knowledge the earliest usage of general binders in a theorem prover
   is described in \cite{NaraschewskiNipkow99} about a formalisation of the
   algorithm W. This formalisation implements binding in type schemes using a
-  de-Bruijn indices representation. Since type schemes of W contain only a single
-  binder, different indices do not refer to different binders (as in the usual
+  de-Bruijn indices representation. Since type schemes in W contain only a single
+  place where variables are bound, different indices do not refer to different binders (as in the usual
   de-Bruijn representation), but to different bound variables. A similar idea
   has been recently explored for general binders in the locally nameless
   approach to binding \cite{chargueraud09}.  There, de-Bruijn indices consist
@@ -2093,7 +2093,8 @@
   representations have to resort to the iterated-single-binders-approach with
   all the unwanted consequences when reasoning about the resulting terms.
 
-  Two formalisations involving general binders have also been performed in older
+  In a similar fashion, two formalisations involving general binders have been 
+  performed in older
   versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W 
   \cite{BengtsonParow09, UrbanNipkow09}).  Both
   use the approach based on iterated single binders. Our experience with