--- 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