--- a/Paper/Paper.thy	Thu Apr 01 14:53:14 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 15:41:48 2010 +0200
@@ -1467,8 +1467,8 @@
 text {*
   Having made all crucial definitions for raw terms, we can start introducing
   the resoning infrastructure for the types the user specified. For this we first
-  have to show that the alpha-equivalence relation defined in the previous
-  sections are indeed equivalence relations. 
+  have to show that the alpha-equivalence relations defined in the previous
+  section are indeed equivalence relations. 
 
   \begin{lemma} 
   Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions
@@ -1491,11 +1491,14 @@
   "C"}$_{1..m}$. Similarly for the free-variable functions @{text
   "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 
-  creating a new type in Isabelle/HOL (remember the picture shown in the 
+  user, since the are formulated in terms of the isomorphisms we obtained by 
+  creating new types in Isabelle/HOL (recall the picture shown in the 
   Introduction).
 
-  {\bf TODO below.}
+  The first usefull property about term-constructors @{text
+  "C"}$^\alpha_{1..m}$ is to know that they are distinct, that is
+  @{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} 
+  @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.
 
   then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
   the raw definitions to the quotient type, we need to prove that they

--- a/Paper/document/root.tex	Thu Apr 01 14:53:14 2010 +0200
+++ b/Paper/document/root.tex	Thu Apr 01 15:41:48 2010 +0200
@@ -63,7 +63,6 @@
 \affiliation{TU Munich, Germany}
 \maketitle
 
-\maketitle
 \begin{abstract} 
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
 prover. It provides a proving infrastructure for convenient reasoning about