  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.
