--- a/Paper/document/root.tex	Wed Mar 17 20:42:42 2010 +0100
+++ b/Paper/document/root.tex	Thu Mar 18 00:17:21 2010 +0100
@@ -1,41 +1,24 @@
 \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
-
-%\usepackage{amssymb}
-  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
-  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
-  %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage[greek,english]{babel}
-  %option greek for \<euro>
-  %option english (default language) for \<guillemotleft>, \<guillemotright>
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
 
-%\usepackage[latin1]{inputenc}
-  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
-  %\<threesuperior>, \<threequarters>, \<degree>
-
-%\usepackage[only,bigsqcap]{stmaryrd}
-  %for \<Sqinter>
+%\ConferenceShortName{ICFP}
+%\ConferenceName{International Conference on Functional Programming}
 
-%\usepackage{eufrak}
-  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
-  %for \<cent>, \<currency>
-
-% this should be the last package used
 \usepackage{pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymiota}{}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+
+
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
 
@@ -51,7 +34,7 @@
 
 \begin{document}
 
-\title{\LARGE\bf General Binding Structures in Nominal Isabelle, or How to
+\title{\LARGE\bf General Binding Structures in Nominal Isabelle,\\ or How to
   Formalise Core-Haskell}
 \maketitle
 
@@ -64,13 +47,16 @@
 are important in formalisation ...
 \end{abstract}
 
+%\begin{keywords}
+%Language formalisations, Isabelle/HOL, POPLmark
+%\end{keywords}
+
+
 % generated text of all theories
 \input{session}
 
-%\bibliographystyle{plain}
-% optional bibliography
-%\bibliographystyle{abbrv}
-%\bibliography{root}
+\bibliographystyle{plain}
+\bibliography{root}
 
 \end{document}