--- a/Paper/Paper.thy	Wed Mar 17 15:13:31 2010 +0100
+++ b/Paper/Paper.thy	Wed Mar 17 17:10:19 2010 +0100
@@ -7,13 +7,38 @@
 section {* Introduction *}
 
 text {*
-  Here can come any text.
+
+  It has not yet fared so well in the POPLmark challenge
+  as the second part contain a formalisation of records 
+  where ...
+
+  The difficulty can be appreciated by considering that the
+  definition given by Leroy in [] is incorrect (it omits a
+  side-condition).
+
+  Examples: type-schemes
+
+  Contributions:  We provide definitions for when terms
+  involving general bindings are alpha-equivelent.
+*}
+
+text {* A Brief Overview about the Nominal Logic Work *}
+
+text {* Abstractions *}
+
+text {* Alpha-Equivalence and Free Variables *}
+
+
+text {*
+  Acknowledgements: We thank Andrew Pitts for the many discussions
+  about the topic. We thank Peter Sewell for making [] available 
+  to us and explaining some of the finer points of the OTT tool.
+
 
 *}
 
 
 
-
 (*<*)
 end
 (*>*)
\ No newline at end of file