--- a/Pearl-jv/Paper.thy	Wed Mar 16 20:42:14 2011 +0100
+++ b/Pearl-jv/Paper.thy	Wed Mar 16 21:07:50 2011 +0100
@@ -67,12 +67,17 @@
   At its core Nominal Isabelle is based on the nominal logic work by Pitts at
   al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a
   sort-respecting permutation operation defined over a countably infinite
-  collection of sorted atoms. The atoms are used for representing variable names
-  that might be bound or free. Multiple sorts are necessary for being able to
-  represent different kinds of variables. For example, in the language Mini-ML
-  there are bound term variables in lambda abstractions and bound type variables in
-  type schemes. In order to be able to separate them, each kind of variables needs to be
-  represented by a different sort of atoms. 
+  collection of sorted atoms. The aim of this paper is to describe how to
+  adapt this work so that it can be implemented in a theorem prover based
+  on Higher-Order Logic (HOL). For this we present the definition we made
+  in the implementation and also review many proofs. There are a two main 
+  design choices to be made. One is
+  how to represent sorted atoms. We opt here for a single unified atom type to
+  represent atoms of different sorts. The other is how to present sort-respecting
+  permutations. For them we use the standard technique of
+  HOL-formalisations of introducing an appropriate substype of functions from 
+  atoms to atoms.
+
 
   The nominal logic work has been the starting point for a number of proving
   infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by
@@ -151,6 +156,8 @@
 
 
   Two binders
+
+  A preliminary version 
 *}
 
 section {* Sorted Atoms and Sort-Respecting Permutations *}
@@ -158,6 +165,13 @@
 text {*
   The two most basic notions in the nominal logic work are a countably
   infinite collection of sorted atoms and sort-respecting permutations of atoms. 
+  The atoms are used for representing variable names
+  that might be bound or free. Multiple sorts are necessary for being able to
+  represent different kinds of variables. For example, in the language Mini-ML
+  there are bound term variables in lambda abstractions and bound type variables in
+  type schemes. In order to be able to separate them, each kind of variables needs to be
+  represented by a different sort of atoms. 
+
   The existing nominal logic work usually leaves implicit
   the sorting information for atoms and as far as we know leaves out a
   description of how sorts are represented.  In our formalisation, we