equal
deleted
inserted
replaced
66 \noindent |
66 \noindent |
67 At its core Nominal Isabelle is based on the nominal logic work by |
67 At its core Nominal Isabelle is based on the nominal logic work by |
68 Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is |
68 Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is |
69 a sort-respecting permutation operation defined over a countably |
69 a sort-respecting permutation operation defined over a countably |
70 infinite collection of sorted atoms. The aim of this paper is to |
70 infinite collection of sorted atoms. The aim of this paper is to |
71 describe how to adapt this work so that it can be implemented in a |
71 describe how we adapted this work so that it can be implemented in a |
72 theorem prover based on Higher-Order Logic (HOL). For this we |
72 theorem prover based on Higher-Order Logic (HOL). For this we |
73 present the definition we made in the implementation and also review |
73 present the definition we made in the implementation and also review |
74 many proofs. There are a two main design choices to be made. One is |
74 many proofs. There are a two main design choices to be made. One is |
75 how to represent sorted atoms. We opt here for a single unified atom |
75 how to represent sorted atoms. We opt here for a single unified atom |
76 type to represent atoms of different sorts. The other is how to |
76 type to represent atoms of different sorts. The other is how to |