diff -r 3c769bf10e63 -r 2c6851248b3f Pearl-jv/document/root.tex
--- a/Pearl-jv/document/root.tex	Tue May 03 15:39:30 2011 +0100
+++ b/Pearl-jv/document/root.tex	Mon May 09 04:49:58 2011 +0100
@@ -5,6 +5,7 @@
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{mathabx}
+\usepackage{proof}
 \usepackage{longtable}
 \usepackage{graphics}
 \usepackage{pdfsetup}
@@ -47,7 +48,8 @@
 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 formalisation of
+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}