--- a/Paper/Paper.thy	Tue Mar 30 09:00:52 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 09:15:40 2010 +0200
@@ -1090,7 +1090,8 @@
 
   \noindent
   We define them together with the auxiliary free variable functions for
-  binding functions
+  binding functions. Given binding functions of types
+  @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define
 
   \begin{center}
   @{text "fv_bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> atom set"}
@@ -1167,6 +1168,23 @@
   \end{tabular}
   \end{center}
 
+  We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
+  we need to define
+
+  \begin{center}
+  @{text "\<approx>\<^isub>1 :: ty\<^isub>1 \<Rightarrow> ty\<^isub>1 \<Rightarrow> bool \<dots> \<approx>\<^isub>n :: ty\<^isub>n \<Rightarrow> ty\<^isub>n \<Rightarrow> bool"}
+  \end{center}
+
+  \noindent
+  together with the auxiliary equivalences for binding functions. Given binding
+  functions for types @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define
+  \begin{center}
+  @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"}
+  \end{center}
+
+
+
+
 *}
 
 section {* The Lifting of Definitions and Properties *}