equal
deleted
inserted
replaced
35 smoothly adapt this theory to a theorem prover environment, in our case |
35 smoothly adapt this theory to a theorem prover environment, in our case |
36 Isabelle/HOL. We present a formalisation of this work that is based on a |
36 Isabelle/HOL. We present a formalisation of this work that is based on a |
37 unified atom type and that represents permutations by bijective functions from |
37 unified atom type and that represents permutations by bijective functions from |
38 atoms to atoms. Interestingly, we allow swappings, which are permutations |
38 atoms to atoms. Interestingly, we allow swappings, which are permutations |
39 build from two atoms, to be ill-sorted. Furthermore we extend the nominal |
39 build from two atoms, to be ill-sorted. Furthermore we extend the nominal |
40 logic work with names that carry additional information and with abstractions |
40 logic work with names that carry additional information and with a |
41 that bind finite sets of names. |
41 formalisation of abstractions that bind finite sets of names. |
42 \end{abstract} |
42 \end{abstract} |
43 |
43 |
44 % generated text of all theories |
44 % generated text of all theories |
45 \input{session} |
45 \input{session} |
46 |
46 |