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

\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}
\author{Christian Urban} 
\address{Technical University of Munich, Germany}	
\email{urbanc@in.tum.de}

\author{Cezary Kaliszyk}
\address{University of Tsukuba, Japan}
\email{kaliszyk@score.cs.tsukuba.ac.jp}

\keywords{Nominal Isabelle, variable convention, formal reasoning}
\subjclass{MANDATORY list of acm classifications}

\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: