\documentclass{svjour3}

\usepackage{times}

\usepackage{isabelle}

\usepackage{isabellesym}

\usepackage{amsmath}

\usepackage{amssymb}

\usepackage{longtable}

\usepackage{pdfsetup}

\urlstyle{rm}

\isabellestyle{it}

\renewcommand{\isastyle}{\isastyleminor}

\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}

\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

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

\renewcommand{\isasymiota}{}

\renewcommand{\isasymrightleftharpoons}{}

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

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

\begin{document}

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

\author{Christian Urban \and Brian Huffman}

\institute{C.~Urban \at Technical University of Munich 

     \and  B.~Huffman \at Portland State University}

\date{Received: date / Accepted: date}

\maketitle

\begin{abstract}

Pitts et al introduced a beautiful theory about names and binding based on the

notions of atoms, permutations and support. The engineering challenge is to

smoothly adapt this theory to a theorem prover environment, in our case

Isabelle/HOL. For this we have to formulate the theory so that it is

and that represents permutations by bijective functions from atoms to atoms. 

Interestingly, we allow swappings, which are permutations build from two

\end{abstract}

% generated text of all theories

\input{session}

% optional bibliography

\bibliographystyle{abbrv}

\bibliography{root}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: t

%%% End: