--- a/Pearl/Paper.thy	Fri Apr 09 08:16:08 2010 -0700
+++ b/Pearl/Paper.thy	Fri Apr 09 09:02:54 2010 -0700
@@ -502,11 +502,12 @@
 %
 %text { *
 
-  One huge advantage of using bijective permutation functions (as opposed to
-  non-bijective renaming substitutions employed in traditional works on syntax) is 
-  the property of \emph{equivariance}
-  and the fact that most HOL-functions (this includes constants) whose argument
-  and result types are permutation types satisfy this property:
+  An \emph{equivariant} function or predicate is one that is invariant under
+  the swapping of atoms.  Having a notion of equivariance with nice logical
+  properties is a major advantage of bijective permutations over traditional
+  renaming substitutions \cite[\S2]{Pitts03}.  Equivariance can be defined
+  uniformly for all permutation types, and it is satisfied by most HOL
+  functions and constants.
 
   \begin{definition}\label{equivariance}
   A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.