--- a/Paper/Paper.thy	Wed Mar 17 17:11:23 2010 +0100
+++ b/Paper/Paper.thy	Wed Mar 17 20:42:22 2010 +0100
@@ -16,17 +16,18 @@
   definition given by Leroy in [] is incorrect (it omits a
   side-condition).
 
-  Examples: type-schemes
+  Examples: type-schemes, Spi-calculus
 
   Contributions:  We provide definitions for when terms
   involving general bindings are alpha-equivelent.
 *}
 
-text {* A Brief Overview about the Nominal Logic Work *}
+section {* A Brief Overview about the Nominal Logic Work *}
 
-text {* Abstractions *}
+section {* Abstractions *}
 
-text {* Alpha-Equivalence and Free Variables *}
+section {* Alpha-Equivalence and Free Variables *}
+
 
 
 text {*