diff -r 66ef2a2c64fb -r c3ff26204d2a Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Fri Apr 22 00:18:25 2011 +0800 +++ b/Pearl-jv/Paper.thy Thu Apr 28 11:44:36 2011 +0800 @@ -495,7 +495,7 @@ text {* An important notion in the nominal logic work is - \emph{equivariance}. It will enable us to characterise how + \emph{equivariance}. This notion allows us to characterise how permutations act upon compound statements in HOL by analysing how these statements are constructed. To do so, let us first define \emph{HOL-terms}. They are given by the grammar