--- a/Paper/Paper.thy	Mon Mar 22 18:38:59 2010 +0100
+++ b/Paper/Paper.thy	Tue Mar 23 07:39:10 2010 +0100
@@ -54,8 +54,8 @@
   also there one would like to bind multiple variables at once.
 
   Binding multiple variables has interesting properties that cannot be captured
-  easily by iterating single binders. For example in the case of type-schemes we do not
-  like to make a distinction about the order of the bound variables. Therefore
+  easily by iterating single binders. For example in case of type-schemes we do not
+  want to make a distinction about the order of the bound variables. Therefore
   we would like to regard the following two type-schemes as alpha-equivalent
   %
   \begin{equation}\label{ex1}
@@ -63,14 +63,15 @@
   \end{equation}
 
   \noindent
-  but  the following two should \emph{not} be alpha-equivalent
+  but assuming that $x$, $y$ and $z$ are distinct variables,
+  the following two should \emph{not} be alpha-equivalent
   %
   \begin{equation}\label{ex2}
   \forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z 
   \end{equation}
 
   \noindent
-  assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as 
+  Moreover, we like to regard type-schemes as 
   alpha-equivalent, if they differ only on \emph{vacuous} binders, such as
   %
   \begin{equation}\label{ex3}
@@ -87,7 +88,7 @@
 
   However, the notion of alpha-equivalence that is preserved by vacuous binders is not
   always wanted. For example in terms like
-
+  %
   \begin{equation}\label{one}
   \LET x = 3 \AND y = 2 \IN x\,-\,y \END
   \end{equation}
@@ -96,7 +97,7 @@
   we might not care in which order the assignments $x = 3$ and $y = 2$ are
   given, but it would be unusual to regard \eqref{one} as alpha-equivalent 
   with
-
+  %
   \begin{center}
   $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$
   \end{center}
@@ -109,7 +110,7 @@
   However, we found that this is still not sufficient for dealing with
   language constructs frequently occurring in programming language
   research. For example in $\mathtt{let}$s containing patterns
-
+  %
   \begin{equation}\label{two}
   \LET (x, y) = (3, 2) \IN x\,-\,y \END
   \end{equation}
@@ -118,7 +119,7 @@
   we want to bind all variables from the pattern inside the body of the
   $\mathtt{let}$, but we also care about the order of these variables, since
   we do not want to regard \eqref{two} as alpha-equivalent with
-
+  %
   \begin{center}
   $\LET (y, x) = (3, 2) \IN x\,- y\,\END$
   \end{center}
@@ -131,7 +132,7 @@
   By providing these general binding mechanisms, however, we have to work around 
   a problem that has been pointed out by Pottier in \cite{Pottier06}: in 
   $\mathtt{let}$-constructs of the form
-
+  %
   \begin{center}
   $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
   \end{center}
@@ -141,7 +142,7 @@
   which the $x_i = t_i$ are given, but we do care about the information that there are 
   as many $x_i$ as there are $t_i$. We lose this information if we represent the 
   $\mathtt{let}$-constructor by something like 
-
+  %
   \begin{center}
   $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$
   \end{center}
@@ -154,7 +155,7 @@
   lists are of equal length. This can result into very messy reasoning (see
   for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications
   for $\mathtt{let}$s as follows
-
+  %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
   $trm$ & $::=$  & \ldots\\ 
@@ -385,10 +386,10 @@
 section {* General Binders *}
 
 text {*
-  In Nominal Isabelle the user is expected to write down a specification of a
-  term-calculus and a reasoning infrastructure is then automatically derived
+  In Nominal Isabelle, the user is expected to write down a specification of a
+  term-calculus and then a reasoning infrastructure is automatically derived
   from this specifcation (remember that Nominal Isabelle is a definitional
-  extension of Isabelle/HOL and cannot introduce new axioms).
+  extension of Isabelle/HOL, which does not introduce any new axioms).
 
 
   In order to keep our work manageable, we will wherever possible state
@@ -508,11 +509,50 @@
   \begin{proof}
   All properties are by unfolding the definitions and simple calculations. 
   \end{proof}
+
+
+  \begin{lemma}
+  $supp ([as]set. x) = supp x - as$ 
+  \end{lemma}
 *}
 
 section {* Alpha-Equivalence and Free Variables *}
 
 text {*
+  A specification of a term-calculus in Nominal Isabelle is a collection
+  of (possibly mutual recursive) type declarations, say $ty_1$, $ty_2$, \ldots $ty_n$ 
+  written as follows:
+
+  \begin{center}
+  \begin{tabular}{l}
+  \isacommand{nominal\_datatype} $ty_1 =$\\
+  \isacommand{and} $ty_2 =$\\
+  $\ldots$\\ 
+  \isacommand{and} $ty_n =$\\ 
+  $\ldots$\\
+  \isacommand{with}\\
+  $\ldots$\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The section below the \isacommand{with} are binding functions, which
+  will be explained below.
+  
+
+
+  A specification of a term-calculus in Nominal Isabell is very similar to 
+  the usual datatype definition of Isabelle/HOL: 
+
+
+  Because of the problem Pottier pointed out in \cite{Pottier06}, the general 
+  binders from the previous section cannot be used directly to represent w 
+  be used directly 
+*}
+
+
+
+text {*
   Restrictions
 
   \begin{itemize}