Paper/Paper.thy
changeset 2518 7044f796d8d1
parent 2517 e1093e680bcf
child 2519 3e9b4ce0aeca
equal deleted inserted replaced
2517:e1093e680bcf 2518:7044f796d8d1
  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