2 \usepackage{times}

     2 \usepackage{times}

     3 \usepackage{isabelle}

     3 \usepackage{isabelle}

     4 \usepackage{isabellesym}

     4 \usepackage{isabellesym}

     5 \usepackage{amsmath}

     5 \usepackage{amsmath}

     6 \usepackage{amssymb}

     6 \usepackage{amssymb}

     7 \usepackage{longtable}

     8 \usepackage{longtable}

     8 \usepackage{graphics}

     9 \usepackage{graphics}

     9 \usepackage{pdfsetup}

    10 \usepackage{pdfsetup}

    10 

    11 

    11 \urlstyle{rm}

    12 \urlstyle{rm}

    17 \renewcommand{\isasymequiv}{$\dn$}

    18 \renewcommand{\isasymequiv}{$\dn$}

    18 \renewcommand{\isasymiota}{}

    19 \renewcommand{\isasymiota}{}

    19 \renewcommand{\isasymrightleftharpoons}{}

    20 \renewcommand{\isasymrightleftharpoons}{}

    20 \renewcommand{\isasymemptyset}{$\varnothing$}

    21 \renewcommand{\isasymemptyset}{$\varnothing$}

    21 \newcommand{\isasymallatoms}{\ensuremath{\mathbb{A}}}

    22 \newcommand{\isasymallatoms}{\ensuremath{\mathbb{A}}}

    22 

    24 

    23 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}

    25 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}

    24 \newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}}

    26 \newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}}

    25 

    29 

    26 \begin{document}

    30 \begin{document}

    27 

    31 

    28 \title{Implementing the Nominal Logic Work in Isabelle/HOL}

    32 \title{Implementing the Nominal Logic Work in Isabelle/HOL}

    29 \author{Christian Urban \and Brian Huffman}

    33 \author{Christian Urban \and Brian Huffman}