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{mathabx}

     7 \usepackage{mathabx}

     8 \usepackage{longtable}

     9 \usepackage{longtable}

     9 \usepackage{graphics}

    10 \usepackage{graphics}

    10 \usepackage{pdfsetup}

    11 \usepackage{pdfsetup}

    11 

    12 

    12 \urlstyle{rm}

    13 \urlstyle{rm}

    45 theory so that it is compatible with Higher-Order Logic, which the original formulation by

    46 theory so that it is compatible with Higher-Order Logic, which the original formulation by

    46 Pitts is not.  We achieve this by not requiring that every construction has 

    47 Pitts is not.  We achieve this by not requiring that every construction has 

    47 to have finite support. We present a formalisation that is based on a

    48 to have finite support. We present a formalisation that is based on a

    48 unified atom type and that represents permutations by bijective functions from

    49 unified atom type and that represents permutations by bijective functions from

    49 atoms to atoms. Interestingly, we allow swappings, which are permutations

    50 atoms to atoms. Interestingly, we allow swappings, which are permutations

    51 two abstraction operators that bind sets of names.

    53 two abstraction operators that bind sets of names.

    52 \end{abstract}

    54 \end{abstract}

    53 

    55 

    54 % generated text of all theories

    56 % generated text of all theories

    55 \input{session}

    57 \input{session}