--- a/Paper/Paper.thy	Thu Apr 01 16:08:54 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 16:17:56 2010 +0200
@@ -1112,7 +1112,7 @@
   The datatype definition can be obtained by stripping off the 
   binding clauses and the labels on the types. We also have to invent
   new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
-  given by user. In our implementation we just use the affix ``@{text "_raw"}''.
+  given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
   But for the purpose of this paper, we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
   that a notion is defined over alpha-equivalence classes and leave it out 
   for the corresponding notion defined on the ``raw'' level. So for example 
@@ -1312,7 +1312,7 @@
   Next we define alpha-equivalence for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
   @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, 
   we also need to  define auxiliary alpha-equivalence relations for the binding functions. 
-  Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>b\<^isub>m"}.
+  Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
   To simplify our definitions we will use the following abbreviations for 
   relations and free-variable acting on products.
   %
@@ -1333,7 +1333,7 @@
 
   \noindent
   For what follows, let us assume 
-  @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}).
+  @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}.
   The task now is to specify what the premises of these clauses are. For this we
   consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will 
   be easier to analyse these pairs according to  ``clusters'' of the binding clauses. 
@@ -1684,7 +1684,6 @@
   \noindent In comparison, the cases for the same constructors in the derived strong
   induction principle are:
 
-%% TODO get rid of the ugly hspaces.
 \begin{equation}\nonumber
 \infer
 {