2 \usepackage{isabelle}

     2 \usepackage{isabelle}

     3 \usepackage{isabellesym}

     3 \usepackage{isabellesym}

     4 \usepackage{amsmath}

     4 \usepackage{amsmath}

     5 \usepackage{amssymb}

     5 \usepackage{amssymb}

     6 \usepackage{amsthm}

     6 \usepackage{amsthm}

    58 

    58 

    59 

    59 

    60 \begin{document}

    60 \begin{document}

    61 

    61 

    62 \title{\LARGE\bf General Bindings and Alpha-Equivalence in Nominal Isabelle}

    62 \title{\LARGE\bf General Bindings and Alpha-Equivalence in Nominal Isabelle}

    65 \maketitle

    66 \maketitle

    66 

    67 

    67 \begin{abstract} 

    68 \begin{abstract} 

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

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

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

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

    77 automatically the reasoning infrastructure for alpha-equated terms. We

    78 automatically the reasoning infrastructure for alpha-equated terms. We

    78 also prove strong induction principles that have the usual variable

    79 also prove strong induction principles that have the usual variable

    79 convention already built in.

    80 convention already built in.

    80 \end{abstract}

    81 \end{abstract}

    81 

    82 

    82 

    91 

    83 \input{session}

    92 \input{session}

    84 

    93 

    85 \bibliographystyle{plain}

    94 \bibliographystyle{plain}

    86 \bibliography{root}

    95 \bibliography{root}