\documentclass{lmcs}
%%\usepackage{times}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
%%\usepackage{amsthm}
\usepackage{tikz}
\usepackage{pgf}
\usepackage{ot1patch}
\usepackage{times}
\usepackage{boxedminipage}
\usepackage{proof}
\usepackage{setspace}
\usepackage{afterpage}
\usepackage{pdfsetup}

\allowdisplaybreaks
\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastyle}{\normalsize\it}%

\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\hspace{-0.5mm}\cdot\hspace{-0.5mm}}$}}}
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{$\dn$}
%%\renewcommand{\isasymiota}{}
\renewcommand{\isasymxi}{$..$}
\renewcommand{\isasymemptyset}{$\varnothing$}
\newcommand{\isasymnotapprox}{$\not\approx$}
\newcommand{\isasymLET}{$\mathtt{let}$}
\newcommand{\isasymAND}{$\mathtt{and}$}
\newcommand{\isasymIN}{$\mathtt{in}$}
\newcommand{\isasymEND}{$\mathtt{end}$}
\newcommand{\isasymBIND}{$\mathtt{bind}$}
\newcommand{\isasymANIL}{$\mathtt{anil}$}
\newcommand{\isasymACONS}{$\mathtt{acons}$}
\newcommand{\isasymCASE}{$\mathtt{case}$}
\newcommand{\isasymOF}{$\mathtt{of}$}
\newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}}
\newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}}
\newcommand{\isasymFRESH}{\#}
\newcommand{\LET}{\;\mathtt{let}\;}
\newcommand{\IN}{\;\mathtt{in}\;}
\newcommand{\END}{\;\mathtt{end}\;}
\newcommand{\AND}{\;\mathtt{and}\;}
\newcommand{\fv}{\mathit{fv}}

\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
%----------------- theorem definitions ----------
%%\theoremstyle{plain}
%%\spnewtheorem{thm}[section]{Theorem}
%%\newtheorem{property}[thm]{Property}
%%\newtheorem{lemma}[thm]{Lemma}
%%\spnewtheorem{defn}[theorem]{Definition}
%%\spnewtheorem{exmple}[theorem]{Example}
%%\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily}
%-------------------- environment definitions -----------------
\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}

%\addtolength{\textwidth}{2mm}
\addtolength{\parskip}{-0.33mm}
\begin{document}

\title[Genral Bindings]{General Bindings and Alpha-Equivalence in Nominal
Isabelle$^\star$}
\author{Christian Urban} 
\address{King's College London, United Kingdom}	
\email{christian.urban@kcl.ac.uk}

\author{Cezary Kaliszyk}
\address{University of Innsbruck, Austria}
\email{cezary.kaliszyk@uibk.ac.at}
\thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}}

\keywords{Nominal Isabelle, variable convention, theorem provers, formal reasoning, lambda-calculus}
\subjclass{F.3.1}

\begin{abstract} 
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
prover. It provides a proving infrastructure for reasoning about
programming language calculi involving named bound variables (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 general
bindings are ubiquitous in programming language research and only very
poorly supported with single binders, such as lambda-abstractions. Our
extension includes new definitions of alpha-equivalence and establishes
automatically the reasoning infrastructure for alpha-equated terms. We
also prove strong induction principles that have the usual variable
convention already built in.
\end{abstract}

\maketitle
\input{session}

\bibliographystyle{plain}
\bibliography{root}


%\pagebreak
%\input{Appendix} 

\end{document}

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