--- a/Paper/Paper.thy	Fri Apr 02 07:43:22 2010 +0200
+++ b/Paper/Paper.thy	Fri Apr 02 07:59:03 2010 +0200
@@ -1807,23 +1807,31 @@
   of the definitions. 
   \end{proof}
 
+  \noindent
   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. 
+  effect on the free-variable function. The main point of this permutation
+  function, however, is that if we have a permutation that is fresh 
+  for the support of an object @{text x}, then we can use this permutation 
+  to rename the binders, without ``changing'' the term. In case of the 
+  @{text "Let"} term-constructor from the example shown 
+  in \eqref{letpat} this means:
 
-  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}
+  if @{term "supp (Abs_lst (bn p) t)  \<sharp>* q"} then @{text "Let p t = Let (q \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) (q \<bullet> t)"}
+  \end{center}
+
+  \noindent
+  This fact will be used when establishing the strong induction principles. 
+  They state that instead of establishing the implication 
 
   \begin{center}
   @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
   \end{center}
 
   \noindent
-  for the weak induction principle, we will show that it is sufficient
-  to establish
+  it is sufficient to establish the following implication
   
   \begin{center}
   \begin{tabular}{l}
@@ -1835,11 +1843,11 @@
   \end{center}
 
   \noindent 
-  While this implication contains additional arguments (i.e.~@{text c}) and 
-  additional universal quantifications, it is usually easier to establish.
+  While this implication contains an additional argument, @{text c}, and 
+  also 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.
+  chosen by the user 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