--- a/Pearl/Paper.thy	Fri Apr 09 11:08:05 2010 +0200
+++ b/Pearl/Paper.thy	Fri Apr 09 08:16:08 2010 -0700
@@ -216,9 +216,12 @@
   simple formalisation of the nominal logic work.\smallskip
 
   \noindent
-  {\bf Contributions of the paper:} The main contribution of this paper is in 
-  showing an example of how theorem proving tools can be improved by getting 
-  the right level of abstraction for the underlying theory.
+  {\bf Contributions of the paper:} Using a single atom type to represent
+  atoms of different sorts and representing permutations as functions are not
+  new ideas.  The main contribution of this paper is to show an example of how
+  to make better theorem proving tools by choosing the right level of
+  abstraction for the underlying theory---our design choices take advantage of
+  Isabelle's type system, type classes, and reasoning infrastructure.
   The novel
   technical contribution is a mechanism for dealing with
   ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages