
diff -r b9caceeec805 -r 9923b2cee778 Paper/document/root.tex
--- a/Paper/document/root.tex	Wed Mar 17 18:52:59 2010 +0100
+++ b/Paper/document/root.tex	Wed Mar 17 18:53:23 2010 +0100
@@ -1,6 +1,9 @@
-\documentstyle[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
 
@@ -45,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
@@ -53,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




