--- a/Paper/Paper.thy	Thu Apr 01 09:28:03 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 10:57:49 2010 +0200
@@ -37,7 +37,7 @@
 section {* Introduction *}
 
 text {*
-  @{text "(1, (2, 3))"}
+%%%  @{text "(1, (2, 3))"}
 
   So far, Nominal Isabelle provides a mechanism for constructing
   alpha-equated terms, for example
@@ -1204,7 +1204,7 @@
   either the corresponding binders are all shallow or there is a single deep binder.
   In the former case we take @{text bnds} to be the union of all shallow 
   binders; in the latter case, we just take the set of atoms specified by the 
-  corrsponding binding function. The value for @{text "x\<^isub>i"} is then given by:
+  corresponding binding function. The value for @{text "x\<^isub>i"} is then given by:
   %
   \begin{equation}\label{deepbody}
   \mbox{%
@@ -1295,7 +1295,7 @@
   "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
   free in @{text "as"}. This is what the purpose of the function @{text
   "fv\<^bsub>bn\<^esub>"} is.  In contrast, in @{text "Let_rec"} we have a
-  recursive binder where we want to also bind all occurences of the atoms
+  recursive binder where we want to also bind all occurrences of the atoms
   @{text "bn as"} inside @{text "as"}. Therefore we have to subtract @{text
   "set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from
   @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is
@@ -1409,7 +1409,7 @@
   {\bf TODO (I do not understand the definition below yet).} 
 
   The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
-  for their respective types, the difference is that they ommit checking the arguments that
+  for their respective types, the difference is that they omit checking the arguments that
   are bound. We assumed that there are no bindings in the type on which the binding function
   is defined so, there are no permutations involved. For a binding function clause 
   @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
@@ -1494,7 +1494,7 @@
   "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
   "bn"}$^\alpha_{1..k}$. However, these definitions are of not much use for the 
   user, since the are formulated in terms of the isomorphism we obtained by 
-  cerating a new type in Isabelle/HOL (remember the picture shown in the 
+  creating a new type in Isabelle/HOL (remember the picture shown in the 
   Introduction).
 
   {\bf TODO below.}
@@ -1572,14 +1572,14 @@
 % Very vague...
   \begin{lemma} For each lifted type @{text "ty\<^isup>\<alpha>\<^isub>i"}, for every @{text "x"}
    of this type:
-  \begin{center}
+  \begin{equation}
   @{term "supp x = fv_ty\<^isup>\<alpha>\<^isub>i x"}.
-  \end{center}
+  \end{equation}
   \end{lemma}
   \begin{proof}
   We will show this by induction together with equations that characterize
   @{term "fv_bn\<^isup>\<alpha>\<^isub>"} in terms of @{term "alpha_bn\<^isup>\<alpha>"}. For each of @{text "fv_bn\<^isup>\<alpha>"}
-  functions this equaton is:
+  functions this equation is:
   \begin{center}
   @{term "{a. infinite {b. \<not> alpha_bn\<^isup>\<alpha> ((a \<rightleftharpoons> b) \<bullet> x) x}} = fv_bn\<^isup>\<alpha> x"}
   \end{center}
@@ -1625,16 +1625,18 @@
   \end{center}
 
   The definition of @{text "\<bullet>bn"} is respectful (simple induction) so we can lift it
-  and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this defnition is correct is:
+  and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this definition is correct is:
 
 %% We could get this from ExLet/perm_bn lemma.
   \begin{lemma} For every bn function  @{text "bn\<^isup>\<alpha>\<^isub>i"},
-  \begin{center}
-  @{text "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i l = bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i l)"}
-  \end{center}
+  \begin{eqnarray}
+  @{term "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i x"} & = & @{term "bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}\\
+  @{term "fv_bn\<^isup>\<alpha>\<^isub>i x"} & = & @{term "fv_bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}
+  \end{eqnarray}
   \end{lemma}
   \begin{proof} By induction on the lifted type it follows from the definitions of
-    permutations on the lifted type and the lifted defining eqautions of @{text "\<bullet>bn"}.
+    permutations on the lifted type and the lifted defining equations of @{text "\<bullet>bn"}
+    and @{text "fv_bn"}.
   \end{proof}
 
 *}
@@ -1844,6 +1846,7 @@
   \item finitely supported abstractions
   \item respectfulness of the bn-functions\bigskip
   \item binders can only have a ``single scope''
+  \item in particular "bind a in b, bind b in c" is not allowed.
   \item all bindings must have the same mode
   \end{itemize}
 *}