\documentclass{acmconf}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}

%\ConferenceShortName{ICFP}
%\ConferenceName{International Conference on Functional Programming}

\usepackage{pdfsetup}
\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}

%----------------- theorem definitions ----------
\newtheorem{Theorem}{Theorem}[section]
\newtheorem{Definition}[Theorem]{Definition}
\newtheorem{Example}{\it Example}[section]

%-------------------- environment definitions -----------------
\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
  Formalise Core-Haskell}
\maketitle

\maketitle
\begin{abstract} 
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}

%\begin{keywords}
%Language formalisations, Isabelle/HOL, POPLmark
%\end{keywords}


% generated text of all theories
\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: