diff -r a6f3e1b08494 -r b6873d123f9b Pearl-jv/document/root.tex
--- a/Pearl-jv/document/root.tex	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-\documentclass{svjour3}
-\usepackage{times}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{mathabx}
-\usepackage{proof}
-\usepackage{longtable}
-\usepackage{graphics}
-\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{\isasymallatoms}{\ensuremath{\mathbb{A}}}
-\newcommand{\rrh}{\mbox{\footnotesize$\rightrightharpoons$}}
-
-\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
-\newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}}
-
-\changenotsign
-
-\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}
-In his nominal logic work, Pitts 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 compatible with Higher-Order Logic, which the original formulation by
-Pitts is not.  We achieve this by not requiring that every construction has 
-to have finite support. We present a formalisation that is based on a
-unified atom type and that represents permutations by bijective functions from
-atoms to atoms. Interestingly, we allow swappings, which are permutations
-build from two atoms, to be ill-sorted.  We also describe a reasoning infrastructure
-that automates properties about equivariance, and present a formalisation of
-two abstraction operators that bind 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: