updated to explicit set type constructor (post Isabelle 3rd January)
\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 NominalIsabelle$^\star$}\author{Christian Urban} \address{Technical University of Munich, Germany} \email{urbanc@in.tum.de}\author{Cezary Kaliszyk}\address{University of Tsukuba, Japan}\email{kaliszyk@cs.tsukuba.ac.jp}\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 theoremprover. It provides a proving infrastructure for reasoning aboutprogramming language calculi involving named bound variables (asopposed to de-Bruijn indices). In this paper we present an extension ofNominal Isabelle for dealing with general bindings, that meansterm-constructors where multiple variables are bound at once. Such generalbindings are ubiquitous in programming language research and only verypoorly supported with single binders, such as lambda-abstractions. Ourextension includes new definitions of alpha-equivalence and establishesautomatically the reasoning infrastructure for alpha-equated terms. Wealso prove strong induction principles that have the usual variableconvention 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: