6 \usepackage{amsthm}

     6 \usepackage{amsthm}

     7 \usepackage{tikz}

     7 \usepackage{tikz}

     8 \usepackage{pgf}

     8 \usepackage{pgf}

     9 \usepackage{pdfsetup}

     9 \usepackage{pdfsetup}

    10 \usepackage{ot1patch}

    10 \usepackage{ot1patch}

    11 

    12 

    12 \urlstyle{rm}

    13 \urlstyle{rm}

    13 \isabellestyle{it}

    14 \isabellestyle{it}

    14 

    15 

    15 \DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}

    16 \DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}

    48 

    49 

    49 \maketitle

    50 \maketitle

    50 \begin{abstract} 

    51 \begin{abstract} 

    51 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem

    52 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem

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

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

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

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

    55 Nominal Isabelle for dealing with general bindings, that means

    56 Nominal Isabelle for dealing with general bindings, that means

    56 term-constructors where multiple variables are bound at once. Such binding

    57 term-constructors where multiple variables are bound at once. Such binding

    57 structures are ubiquitous in programming language research and only very

    58 structures are ubiquitous in programming language research and only very

    58 poorly supported with single binders, such as lambda-abstractions. Our

    59 poorly supported with single binders, such as lambda-abstractions. Our