Pearl/Paper.thy
changeset 1790 000e680b6b6e
parent 1784 a862a3befe37
child 1791 c127cfcba764
--- a/Pearl/Paper.thy	Thu Apr 08 09:13:36 2010 +0200
+++ b/Pearl/Paper.thy	Thu Apr 08 10:25:13 2010 +0200
@@ -216,12 +216,11 @@
   simple formalisation of the nominal logic work.\smallskip
 
   \noindent
-  {\bf Contributions of the paper:} Our use of a single atom type for representing
-  atoms of different sorts and of functions for representing
-  permutations is not novel, but drastically reduces the number of type classes to just
-  two (permutation types and finitely supported types) that we need in order
-  reason abstractly about properties from the nominal logic work. The novel
-  technical contribution of this paper is a mechanism for dealing with
+  {\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.
+  The novel
+  technical contribution is a mechanism for dealing with
   ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages
   \cite{PittsHOL4} where variables and variable binding depend on type
   annotations.
@@ -501,7 +500,7 @@
 %text { *
 
   One huge advantage of using bijective permutation functions (as opposed to
-  non-bijective renaming substitutions employed in traditional works syntax) is 
+  non-bijective renaming substitutions employed in traditional works on syntax) is 
   the property of \emph{equivariance}
   and the fact that most HOL-functions (this includes constants) whose argument
   and result types are permutation types satisfy this property:
@@ -890,10 +889,10 @@
 
   The following Isabelle/HOL command defines a concrete atom type called
   \emph{name}, which consists of atoms whose sort equals the string @{term
-  "''Thy.name''"}.
+  "''name''"}.
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''Thy.name''}"}
+  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}
   \end{isabelle}
 
   \noindent