diff -r e25b0fff0dd2 -r 409ecb7284dd Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Tue May 11 18:20:25 2010 +0200
+++ b/Pearl-jv/Paper.thy	Wed May 12 13:43:48 2010 +0100
@@ -55,10 +55,16 @@
   there are bound term variables and bound type variables; each kind needs to
   be represented by a different sort of atoms.
 
-  Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
-  atoms and sorts are used in the original formulation of the nominal logic work.
-  The reason is that one has to ensure that permutations are sort-respecting.
-  This was done implicitly in the original nominal logic work \cite{Pitts03}.
+  In our formalisation of the nominal logic work, we have to make a design decision 
+  about how to represent sorted atoms and sort-respecting permutations. One possibility
+  is to 
+
+
+
+%  Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
+%  atoms and sorts are used in the original formulation of the nominal logic work.
+%  The reason is that one has to ensure that permutations are sort-respecting.
+%  This was done implicitly in the original nominal logic work \cite{Pitts03}.
 
 
   Isabelle used the two-place permutation operation with the generic type