\documentclass{acmconf}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{tikz}
\usepackage{pgf}
\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$}



%----------------- theorem definitions ----------
\newtheorem{property}{Property}[section]
\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 proving infrastructure for convenient reasoning about
programming language calculi. In this paper we present an extension of Nominal
Isabelle for dealing with general binding structures. Such binding structures are
ubiquitous in programming language research and only very poorly handled by
single binding from the lambda-calculus. We give in this
paper novel definitions for alpha-equivalence and establish automatically the
reasoning structure for alpha-equated terms. For example we provide a strong
induction principle that has the variable convention already built in.
\end{abstract}


\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}

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