--- a/Pearl-jv/Paper.thy	Fri Apr 08 14:23:28 2011 +0800
+++ b/Pearl-jv/Paper.thy	Sat Apr 09 00:28:53 2011 +0100
@@ -473,8 +473,9 @@
 
 text {*
   An important notion in the nominal logic work is
-  \emph{equivariance}.  To give a definition for this notion, let us
-  define \emph{HOL-terms}. They are given by the grammar
+  \emph{equivariance}.  In order to prove properties about this notion, 
+  let us first define \emph{HOL-terms}. They are given 
+  by the grammar
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}
@@ -482,22 +483,23 @@
   \end{isabelle} 
 
   \noindent
-  whereby @{text c} stands for constants and @{text x} for
-  variables. We assume HOL-terms are fully typed, but for the sake of
-  greater legibility we leave the typing information implicit.  We
-  also assume the usual notions for free and bound variables of a
-  HOL-term.
+  whereby @{text c} stands for constant symbols, or short constants, and
+  @{text x} for variables. We assume HOL-terms are fully typed, but for the
+  sake of greater legibility we leave the typing information implicit.  We
+  also assume the usual notions for free and bound variables of a HOL-term.
 
   An equivariant HOL-term is one that is invariant under the
-  permutation operation. This notion can be defined as follows:
+  permutation operation. This notion can be defined in Isabelle/HOL 
+  as follows:
 
   \begin{definition}[Equivariance]\label{equivariance}
-  A HOL-term @{text t} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> t = t"}.
+  A  HOL-term @{text t} with permutation type is \emph{equivariant} provided 
+  @{term "\<pi> \<bullet> t = t"} holds for all permutations @{text "\<pi>"}.
   \end{definition}
 
   \noindent
   There are a number of equivalent formulations for the equivariance
-  property.  For example, assuming @{text t} is of type @{text "\<alpha> \<Rightarrow>
+  property.  For example, assuming @{text t} is of permutation type @{text "\<alpha> \<Rightarrow>
   \<beta>"}, then equivariance can also be stated as
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -528,7 +530,8 @@
 
   \noindent
   using the permutation operation on booleans and property
-  \eqref{permuteequ}.  Lemma~\ref{permutecompose} establishes that the
+  \eqref{permuteequ}. 
+  Lemma~\ref{permutecompose} establishes that the
   permutation operation is equivariant. The permutation operation for
   lists and products, shown in \eqref{permdefs}, state that the
   constructors for products, @{text "Nil"} and @{text Cons} are
@@ -546,7 +549,7 @@
   @{const True} and @{const False} are equivariant by the definition
   of the permutation operation for booleans.  It is also easy to see
   that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text
-  "\<not>"} and @{text "\<longrightarrow>"} are all equivariant.
+  "\<not>"} and @{text "\<longrightarrow>"} are all equivariant (see ??? intro)
 
   In contrast, the advantage of Definition \ref{equivariance} is that
   it leads to a simple rewrite system. Consider the following oriented