--- a/Paper/Paper.thy	Tue Mar 23 09:05:23 2010 +0100
+++ b/Paper/Paper.thy	Tue Mar 23 10:24:12 2010 +0100
@@ -16,7 +16,7 @@
 
 text {*
   So far, Nominal Isabelle provides a mechanism for constructing
-  alpha-equated terms such as
+  alpha-equated terms, for example
 
   \begin{center}
   $t ::= x \mid t\;t \mid \lambda x. t$
@@ -24,7 +24,7 @@
 
   \noindent
   where free and bound variables have names.  For such terms Nominal Isabelle
-  derives automatically a reasoning infrastructure, which has been used
+  derives automatically a reasoning infrastructure that  has been used
   successfully in formalisations of an equivalence checking algorithm for LF
   \cite{UrbanCheneyBerghofer08}, Typed
   Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
@@ -83,7 +83,7 @@
   In this paper we will give a general binding mechanism and associated
   notion of alpha-equivalence that can be used to faithfully represent
   this kind of binding in Nominal Isabelle.  The difficulty of finding the right notion 
-  for alpha-equivalence in this case can be appreciated by considering that the 
+  for alpha-equivalence can be appreciated in this case by considering that the 
   definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
 
   However, the notion of alpha-equivalence that is preserved by vacuous binders is not
@@ -178,7 +178,7 @@
   The scope of the binding is indicated by labels given to the types, for
   example \mbox{$s\!::\!trm$}, and a binding clause, in this case
   $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the
-  function $bn\,(a)$ returns.  This style of specifying terms and bindings is
+  function call $bn\,(a)$ returns.  This style of specifying terms and bindings is
   heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 
   However, we will not be able to deal with all specifications that are
@@ -191,8 +191,8 @@
 
   \noindent
   where no clause for variables is given. Such specifications make some sense in
-  the context of Coq's type theory (which Ott supports), but not at al in a HOL-based 
-  theorem prover where every datatype must have a non-empty set-theoretic model.
+  the context of Coq's type theory (which Ott supports), but not at all in a HOL-based 
+  environment where every datatype must have a non-empty set-theoretic model.
 
   Another reason is that we establish the reasoning infrastructure
   for alpha-\emph{equated} terms. In contrast, Ott produces  a reasoning 
@@ -221,13 +221,13 @@
   in a representation based on raw terms requires a lot of extra reasoning work.
 
   Although in informal settings a reasoning infrastructure for alpha-equated 
-  terms (that have names for bound variables) is nearly always taken for granted, establishing 
+  terms is nearly always taken for granted, establishing 
   it automatically in the Isabelle/HOL theorem prover is a rather non-trivial task. 
   For every specification we will need to construct a type containing as 
   elements the alpha-equated terms. To do so, we use 
   the standard HOL-technique of defining a new type by  
   identifying a non-empty subset of an existing type.   The construction we 
-  perform in HOL is illustrated by the following picture:
+  perform in HOL can be illustrated by the following picture:
  
   \begin{center}
   \begin{tikzpicture}
@@ -256,25 +256,26 @@
   \noindent
   We take as the starting point a definition of raw terms (defined as a 
   datatype in Isabelle/HOL); identify then the 
-  alpha-equivalence classes in the type of sets of raw terms, according to our 
+  alpha-equivalence classes in the type of sets of raw terms according to our 
   alpha-equivalence relation and finally define the new type as these 
   alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are 
-  definable as datatype in Isabelle/HOL and the fact that our relation for alpha is an 
-  equivalence relation).
+  definable as datatype in Isabelle/HOL and the fact that our relation for 
+  alpha-equivalence is indeed an equivalence relation).
 
-  The fact that we obtain an isomorphism between between the new type and the non-empty 
+  The fact that we obtain an isomorphism between the new type and the non-empty 
   subset shows that the new type is a faithful representation of alpha-equated terms. 
   That is not the case for example in the representation of terms using the locally 
-  nameless representation of binders \cite{McKinnaPollack99}: there are ``junk'' terms that need to
+  nameless representation of binders \cite{McKinnaPollack99}: in this representation 
+  there are ``junk'' terms that need to
   be excluded by reasoning about a well-formedness predicate.
 
   The problem with introducing a new type in Isabelle/HOL is that in order to be useful, 
   a reasoning infrastructure needs to be ``lifted'' from the underlying subset to 
-  the new type. This is usually a tricky and arduous task. To ease it
+  the new type. This is usually a tricky and arduous task. To ease it,
   we re-implemented in Isabelle/HOL the quotient package described by Homeier 
   \cite{Homeier05}. This package 
   allows us to  lift definitions and theorems involving raw terms
-  to definitions and theorems involving alpha-equated terms. For example
+  to definitions and theorems involving alpha-equated, terms. For example
   if we define the free-variable function over lambda terms
 
   \begin{center}
@@ -296,23 +297,25 @@
   \noindent
   (Note that this means also the term-constructors for variables, applications
   and lambda are lifted to the quotient level.)  This construction, of course,
-  only works if alpha is an equivalence relation, and the definitions and theorems 
-  are respectful w.r.t.~alpha-equivalence.  Hence we will not be able to lift this
-  a bound-variable function to alpha-equated terms (since it does not respect
-  alpha-equivalence). To sum up, every lifting needs proofs of some respectfulness
-  properties. These proofs we are able automate and therefore establish a 
-  useful reasoning infrastructure for alpha-equated lambda terms.\medskip
+  only works if alpha-equivalence is an equivalence relation, and the
+  definitions and theorems are respectful w.r.t.~alpha-equivalence.  Hence we
+  will not be able to lift a bound-variable function to alpha-equated terms
+  (since it does not respect alpha-equivalence). To sum up, every lifting of
+  theorems to the quotient level needs proofs of some respectfulness
+  properties. In the paper we show that we are able to automate these
+  proofs and therefore can establish a reasoning infrastructure for
+  alpha-equated terms.\medskip
 
 
   \noindent
   {\bf Contributions:}  We provide new definitions for when terms
   involving multiple binders are alpha-equivalent. These definitions are
-  inspired by earlier work of Pitts \cite{}. By means of automatic
+  inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
   proofs, we establish a reasoning infrastructure for alpha-equated
   terms, including properties about support, freshness and equality
-  conditions for alpha-equated terms. We re also able to derive, at the moment 
-  only manually, for these terms a strong induction principle that 
-  has the variable convention already built in.
+  conditions for alpha-equated terms. We are also able to derive, at the moment 
+  only manually, strong induction principles that 
+  have the variable convention already built in.
 *}
 
 section {* A Short Review of the Nominal Logic Work *}
@@ -525,10 +528,10 @@
 
   \begin{center}
   \begin{tabular}{l}
-  \isacommand{nominal\_datatype} $ty_1 =$\\
-  \isacommand{and} $ty_2 =$\\
+  \isacommand{nominal\_datatype} $ty_{\alpha{}1} =$\\
+  \isacommand{and} $ty_{\alpha{}2} =$\\
   $\ldots$\\ 
-  \isacommand{and} $ty_n =$\\ 
+  \isacommand{and} $ty_{\alpha{}}n =$\\ 
   $\ldots$\\
   \isacommand{with}\\
   $\ldots$\\

--- a/Paper/document/root.bib	Tue Mar 23 09:05:23 2010 +0100
+++ b/Paper/document/root.bib	Tue Mar 23 10:24:12 2010 +0100
@@ -1,3 +1,11 @@
+
+@Unpublished{Pitts04,
+  author = 	 {Andrew Pitts},
+  title = 	 {{N}otes on the {R}estriction {M}onad for {N}ominal {S}ets and {C}pos},
+  note = 	 {bla},
+  year = 	 {2004}
+}
+
 @incollection{UrbanNipkow09,
   author = {C.~Urban and T.~Nipkow},
   title = {{N}ominal {V}erification of {A}lgorithm {W}},

--- a/Paper/document/root.tex	Tue Mar 23 09:05:23 2010 +0100
+++ b/Paper/document/root.tex	Tue Mar 23 10:24:12 2010 +0100
@@ -8,6 +8,7 @@
 \usepackage{pgf}
 \usepackage{pdfsetup}
 \usepackage{ot1patch}
+\usepackage{times}
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -50,7 +51,7 @@
 \begin{abstract} 
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
 prover. It provides a proving infrastructure for convenient reasoning about
-programming language calculi involving bound variables that have names (as
+programming language calculi involving named bound variables (as
 opposed to de-Bruijn indices). In this paper we present an extension of
 Nominal Isabelle for dealing with general bindings, that means
 term-constructors where multiple variables are bound at once. Such binding