diff -r 78d828f43cdf -r 4b4742aa43f2 Pearl/document/root.tex
--- a/Pearl/document/root.tex	Sat Dec 17 16:58:11 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-\documentclass{llncs}
-\usepackage{times}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage{amsmath}
-\usepackage{amssymb}
-
-
-\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{Proof Pearl: A New Foundation for Nominal Isabelle}
-\author{Brian Huffman\inst{1} and Christian Urban\inst{2}}
-\institute{Portland State University \and Technical University of Munich}
-\maketitle
-
-\begin{abstract}
-Pitts et al introduced a beautiful theory about names and binding based on the
-notions of permutation and support. The engineering challenge is to smoothly
-adapt this theory to a theorem prover environment, in our case Isabelle/HOL.
-We present a formalisation of this work that differs from our earlier approach
-in two important respects: First, instead of representing permutations as
-lists of pairs of atoms, we now use a more abstract representation based on
-functions.  Second, whereas the earlier work modeled different sorts of atoms
-using different types, we now introduce a unified atom type that includes all
-sorts of atoms. Interestingly, we allow swappings, that is permutations build from
-two atoms, to be ill-sorted.  As a result of these design changes, we can iron
-out inconveniences for the user, considerably simplify proofs and also
-drastically reduce the amount of custom ML-code. Furthermore we can extend the
-capabilities of Nominal Isabelle to deal with variables that carry additional
-information. We end up with a pleasing and formalised theory of permutations
-and support, on which we can build an improved and more powerful version of
-Nominal Isabelle.
-\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: