# HG changeset patch
# User Brian Huffman <brianh@cs.pdx.edu>
# Date 1270826168 25200
# Node ID d8bd4923b3aa0fb7a8c2b4a845d30f11d259310e
# Parent  fddb470720f11c69c70ec8db5528edaebc9a48a4
edit 'contributions' section so we do not just quote directly from the reviewer

diff -r fddb470720f1 -r d8bd4923b3aa Pearl/Paper.thy
--- 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