equal
deleted
inserted
replaced
214 with the large amounts of custom ML-code for generating multiple variants |
214 with the large amounts of custom ML-code for generating multiple variants |
215 for some basic definitions. The result is that we can implement a pleasingly |
215 for some basic definitions. The result is that we can implement a pleasingly |
216 simple formalisation of the nominal logic work.\smallskip |
216 simple formalisation of the nominal logic work.\smallskip |
217 |
217 |
218 \noindent |
218 \noindent |
219 {\bf Contributions of the paper:} The main contribution of this paper is in |
219 {\bf Contributions of the paper:} Using a single atom type to represent |
220 showing an example of how theorem proving tools can be improved by getting |
220 atoms of different sorts and representing permutations as functions are not |
221 the right level of abstraction for the underlying theory. |
221 new ideas. The main contribution of this paper is to show an example of how |
|
222 to make better theorem proving tools by choosing the right level of |
|
223 abstraction for the underlying theory---our design choices take advantage of |
|
224 Isabelle's type system, type classes, and reasoning infrastructure. |
222 The novel |
225 The novel |
223 technical contribution is a mechanism for dealing with |
226 technical contribution is a mechanism for dealing with |
224 ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages |
227 ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages |
225 \cite{PittsHOL4} where variables and variable binding depend on type |
228 \cite{PittsHOL4} where variables and variable binding depend on type |
226 annotations. |
229 annotations. |