--- a/Pearl-jv/document/root.tex	Mon May 02 13:01:02 2011 +0800
+++ b/Pearl-jv/document/root.tex	Wed May 04 15:27:04 2011 +0800
@@ -47,7 +47,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}