--- a/Paper/Paper.thy	Fri Apr 02 07:30:25 2010 +0200
+++ b/Paper/Paper.thy	Fri Apr 02 07:43:22 2010 +0200
@@ -1666,11 +1666,11 @@
 
   \noindent
   To sum up this section, we established a reasoning infrastructure
-  for the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"} 
+  for the types @{text "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"} 
   by first lifting definitions from the raw level to the quotient level and
   then establish facts about these lifted definitions. All necessary proofs
-  are generated automatically by custom ML-code. This code can deal with 
-  specifications as shown in Figure~\ref{nominalcorehas} for Core-Haskell.  
+  are generated automatically by custom ML-code we implemented. This code can deal with 
+  specifications like the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.  
 
   \begin{figure}[t!]
   \begin{boxedminipage}{\linewidth}
@@ -1759,20 +1759,22 @@
 
   \noindent
   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 
-  The problem with this implication is that in general it is not easy to establish.
+  The problem with this implication is that in general it is not easy to establish this
+  implication
   The reason is we cannot make any assumption about the binders in @{text "C\<^sup>\<alpha>"} 
   (for example we cannot assume the variable convention).
 
   In \cite{UrbanTasson05} we introduced a method for automatically
   strengthening weak induction principles for terms containing single
-  binders. These stronger induction principles allow us to make additional
-  assumptions about binders. These additional assumptions amount to a formal
-  version of the usual variable convention for binders. A natural question is
-  whether we can also strengthen the weak induction principles in the presence
+  binders. These stronger induction principles allow the user to make additional
+  assumptions about binders when proving the induction hypotheses. 
+  These additional assumptions amount to a formal
+  version of the informal variable convention for binders. A natural question is
+  whether we can also strengthen the weak induction principles involving
   general binders. We will indeed be able to so, but for this we need an 
   additional notion of permuting deep binders. 
 
-  Given a binding function @{text "bn"} we need to define an auxiliary permutation 
+  Given a binding function @{text "bn"} we define an auxiliary permutation 
   operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
   Given a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
   %
@@ -1792,12 +1794,12 @@
   \end{center}
   
   \noindent
-  Using the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to alpha
-  equated terms. We can then prove
+  Using the quotient package again we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 
+  alpha-equated terms. We can then prove:
 
-  \begin{lemma} Given a binding function @{text "bn\<^sup>\<alpha>"}. Then 
+  \begin{lemma} Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
   {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"} and {\it ii)}
-  for all permutations @{text p},  @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"}.
+    @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"}.
   \end{lemma}
 
   \begin{proof} 
@@ -1805,8 +1807,14 @@
   of the definitions. 
   \end{proof}
 
-  This allows is to strengthen the induction principles. We will explain
-  the details with the @{text "Let"} term-constructor from \eqref{letpat}.
+  The first property states that a permutation applied to a binding function is
+  equivalent to first permuting the binders and then calculating the bound
+  variables. The second amounts to the fact that permuting the binders has no 
+  effect on the free-variable function. 
+
+  This notion allows is to strengthen the induction principles. We will explain
+  the details with the @{text "Let"} term-constructor from the example shown 
+  in \eqref{letpat}.
   Instead of establishing the implication 
 
   \begin{center}
@@ -1814,7 +1822,7 @@
   \end{center}
 
   \noindent
-  from the weak induction principle, we will show that it is sufficient
+  for the weak induction principle, we will show that it is sufficient
   to establish
   
   \begin{center}
@@ -1826,6 +1834,12 @@
   \end{tabular}
   \end{center}
 
+  \noindent 
+  While this implication contains additional arguments (i.e.~@{text c}) and 
+  additional universal quantifications, it is usually easier to establish.
+  The reason is that in the case of @{text "Let"} we can make the freshness 
+  assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, wherby @{text c} can be arbitrarily 
+  chosen as long as it has finite support.
 
   With the help of @{text "\<bullet>bn"} functions defined in the previous section
   we can show that binders can be substituted in term constructors. We show