--- a/Pearl-jv/document/root.tex	Tue Mar 08 09:07:49 2011 +0000
+++ b/Pearl-jv/document/root.tex	Fri Mar 11 08:51:39 2011 +0000
@@ -5,9 +5,9 @@
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{longtable}
-
+\usepackage{graphics}
+\usepackage{pdfsetup}
 
-\usepackage{pdfsetup}
 \urlstyle{rm}
 \isabellestyle{it}
 \renewcommand{\isastyle}{\isastyleminor}
@@ -18,9 +18,10 @@
 \renewcommand{\isasymiota}{}
 \renewcommand{\isasymrightleftharpoons}{}
 \renewcommand{\isasymemptyset}{$\varnothing$}
+\newcommand{\isasymallatoms}{\ensuremath{\mathbb{A}}}
 
 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
-
+\newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}}
 
 \begin{document}
 
@@ -33,16 +34,17 @@
 \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
-compatible with HOL, which the original formulation by Pitts is not.  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 formalisation of two 
-abstraction operators that bind sets of names.
+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 HOL, which the original formulation by
+Pitts is not.  We achieve this by not requiring that every object in our
+discourse has 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 formalisation of
+two abstraction operators that bind sets of names.
 \end{abstract}
 
 % generated text of all theories