equal
deleted
inserted
replaced
2338 them in others so that they make sense in the context of $\alpha$-equated terms. |
2338 them in others so that they make sense in the context of $\alpha$-equated terms. |
2339 We also introduced two binding modes (set and res) that do not |
2339 We also introduced two binding modes (set and res) that do not |
2340 exist in Ott. |
2340 exist in Ott. |
2341 We have tried out the extension with calculi such as Core-Haskell, type-schemes |
2341 We have tried out the extension with calculi such as Core-Haskell, type-schemes |
2342 and approximately a dozen of other typical examples from programming |
2342 and approximately a dozen of other typical examples from programming |
2343 language research \cite{SewellBestiary}. The code |
2343 language research~\cite{SewellBestiary}. The code |
2344 will eventually become part of the next Isabelle distribution.\footnote{For the moment |
2344 will eventually become part of the next Isabelle distribution.\footnote{For the moment |
2345 it can be downloaded from the Mercurial repository linked at |
2345 it can be downloaded from the Mercurial repository linked at |
2346 \href{http://isabelle.in.tum.de/nominal/download} |
2346 \href{http://isabelle.in.tum.de/nominal/download} |
2347 {http://isabelle.in.tum.de/nominal/download}.} |
2347 {http://isabelle.in.tum.de/nominal/download}.} |
2348 |
2348 |