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}

    57 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{}

    57 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{}

    58 

    58 

    59 

    59 

    60 \begin{document}

    60 \begin{document}

    61 

    61 

    66 \maketitle

    66 \maketitle

    67 

    67 

    68 \begin{abstract} 

    68 \begin{abstract} 

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

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

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

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

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

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

    79 also prove strong induction principles that have the usual variable

    79 also prove strong induction principles that have the usual variable

    80 convention already built in.

    80 convention already built in.

    81 \end{abstract}

    81 \end{abstract}

    82 

    82 

    83 

    91 

    84 \input{session}

    92 \input{session}

    85 

    93 

    86 \bibliographystyle{plain}

    94 \bibliographystyle{plain}

    87 \bibliography{root}

    95 \bibliography{root}