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