49 prover. It provides a proving infrastructure for convenient reasoning about

    49 prover. It provides a proving infrastructure for convenient reasoning about

    50 programming language calculi involving bound variables that have names (as

    50 programming language calculi involving bound variables that have names (as

    51 opposed to de-Bruijn indices). In this paper we present an extension of

    51 opposed to de-Bruijn indices). In this paper we present an extension of

    52 Nominal Isabelle in order to deal with general binding structures. Such

    52 Nominal Isabelle in order to deal with general binding structures. Such

    53 binding structures are ubiquitous in programming language research and only

    53 binding structures are ubiquitous in programming language research and only

    55 lambda-calculus. For our extension we introduce novel definitions of

    55 lambda-calculus. For our extension we introduce novel definitions of

    56 alpha-equivalence and establish automatically the reasoning infrastructure for

    56 alpha-equivalence and establish automatically the reasoning infrastructure for

    57 alpha-equated terms. This includes strong induction principles that have the

    57 alpha-equated terms. This includes strong induction principles that have the

    58 variable convention already built in.

    58 variable convention already built in.

    59 \end{abstract}

    59 \end{abstract}