# HG changeset patch
# User Brian Huffman <brianh@cs.pdx.edu>
# Date 1270828974 25200
# Node ID 6471e252f14e9c311ec612c20731ce8616c99ae0
# Parent  d8bd4923b3aa0fb7a8c2b4a845d30f11d259310e
rewrite paragraph introducing equivariance, add citation to Pitts03

diff -r d8bd4923b3aa -r 6471e252f14e Pearl/Paper.thy
--- 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"}.