\documentclass{acmconf}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{tikz}
\usepackage{pgf}
\usepackage{pdfsetup}
\usepackage{ot1patch}

\urlstyle{rm}
\isabellestyle{it}

\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
\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$}
\newcommand{\LET}{\;\mathtt{let}\;}
\newcommand{\IN}{\;\mathtt{in}\;}
\newcommand{\END}{\;\mathtt{end}\;}
\newcommand{\AND}{\;\mathtt{and}\;}
\newcommand{\fv}{\mathit{fv}}


%----------------- theorem definitions ----------
\theoremstyle{plain}
\newtheorem{thm}{Theorem}[section]
\newtheorem{property}[thm]{Property}
\newtheorem{lemma}[thm]{Lemma}
\newtheorem{defn}[thm]{Definition}
\newtheorem{exmple}[thm]{Example}

%-------------------- environment definitions -----------------
\newenvironment{example}[0]{\begin{Example} \it}{\end{Example}}
\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}


\begin{document}

\title{\LARGE\bf General Bindings 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 proving infrastructure for convenient reasoning about
programming language calculi involving bound variables that have names (as
opposed to de-Bruijn indices). In this paper we present an extension of
Nominal Isabelle for dealing with general bindings, that means
term-constructors where multiple variables are bound at once. Such binding
structures are ubiquitous in programming language research and only very
poorly supported with single binders, such as lambda-abstractions. Our
extension includes novel definitions of alpha-equivalence and establishes
automatically the reasoning infrastructure for alpha-equated terms. We
also provide strong induction principles that have the usual variable
convention already built in.
\end{abstract}


\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}

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