2179 text {* |
2179 text {* |
2180 We have presented an extension of Nominal Isabelle for dealing with |
2180 We have presented an extension of Nominal Isabelle for dealing with |
2181 general binders, that is term-constructors having multiple bound |
2181 general binders, that is term-constructors having multiple bound |
2182 variables. For this extension we introduced novel definitions of |
2182 variables. For this extension we introduced novel definitions of |
2183 $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL. |
2183 $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL. |
2184 To specify general binders we used the syntax from Ott, but modified |
2184 To specify general binders we used the specifications from Ott, but extended them |
2185 it so that it makes sense in our context of $\alpha$-equated terms. |
2185 in some places and restricted |
|
2186 them in others so that they make sense in the context of $\alpha$-equated terms. |
2186 We have tried out the extension with terms from Core-Haskell, type-schemes |
2187 We have tried out the extension with terms from Core-Haskell, type-schemes |
2187 and the lambda-calculus, and our code |
2188 and the lambda-calculus, and our code |
2188 will eventually become part of the next Isabelle distribution.\footnote{For the moment |
2189 will eventually become part of the next Isabelle distribution.\footnote{For the moment |
2189 it can be downloaded from the Mercurial repository linked at |
2190 it can be downloaded from the Mercurial repository linked at |
2190 \href{http://isabelle.in.tum.de/nominal/download} |
2191 \href{http://isabelle.in.tum.de/nominal/download} |