kept the nested structure of constructors (belonging to one datatype)
\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 thenotions of atoms, permutations and support. The engineering challenge is tosmoothly adapt this theory to a theorem prover environment, in our caseIsabelle/HOL. We present a formalisation of this work that is based on aunified atom type and that represents permutations by bijective functions fromatoms to atoms. Interestingly, we allow swappings, which are permutationsbuild from two atoms, to be ill-sorted. Furthermore we extend the nominallogic work with names that carry additional information and with aformalisation of abstractions that bind finite sets of names.\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: