--- a/Nominal/ROOT.ML	Wed Mar 17 15:13:31 2010 +0100
+++ b/Nominal/ROOT.ML	Wed Mar 17 17:10:19 2010 +0100
@@ -5,6 +5,14 @@
     "Nominal2_Eqvt",
     "Nominal2_Atoms",
     "Nominal2_Supp",
+    "Test"]
+
+(*
+no_document use_thys
+   ["Nominal2_Base",
+    "Nominal2_Eqvt",
+    "Nominal2_Atoms",
+    "Nominal2_Supp",
     "Test",
     "Term1",
     "Term2",
@@ -17,3 +25,4 @@
     "Term9",
     "TySch",
     "LFex"];
+*)
\ No newline at end of file

--- 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

--- a/Paper/document/root.tex	Wed Mar 17 15:13:31 2010 +0100
+++ b/Paper/document/root.tex	Wed Mar 17 17:10:19 2010 +0100
@@ -1,7 +1,9 @@
-\documentclass{article}
-%%\documentclass[epsf]{acmconf}
+\documentclass{acmconf}
 \usepackage{isabelle,isabellesym}
 
+\ConferenceShortName{ICFP}
+\ConferenceName{International Conference on Functional Programming}
+
 % further packages required for unusual symbols (see also
 % isabellesym.sty), use only when needed
 
@@ -46,6 +48,7 @@
 \newenvironment{example}[0]{\begin{Example} \it}{\end{Example}}
 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
 
+
 \begin{document}
 
 \title{\LARGE\bf General Binding Structures in Nominal Isabelle, or How to
@@ -54,7 +57,11 @@
 
 \maketitle
 \begin{abstract} 
-TODO
+Nominal Isabelle is a definitional extension of the Isabelle/HOL
+theorem prover. It provides a reasoning infrastructure for formalisations
+of programming language calculi. In this paper we present an extension
+of Nominal Isabelle with general binding constructs. Such constructs
+are important in formalisation ...
 \end{abstract}
 
 % generated text of all theories