Isabelle/UTP

Documentation

For installation, please see the README.md in the GitHub repository. For now, we don’t make specific releases of Isabelle/UTP, but the current version of the master branch is usually stable and can be obtained either as a zip file or tar ball.

For browsing the Isabelle/UTP GitHub repository I recommend the very useful Matisa extension from my colleague Pedro Ribiero which typesets Isabelle using MathJax. It can be obtained for Google Chrome and also for Firefox.

Information on core parts of the UTP can be found under the documentation item in the menu to the right. The following additional materials are also available:

• Isabelle/UTP Tutorial. This covers the basics of Isabelle/UTP, including its lens-based state model and core proof tactics.
• Syntax reference guide. A reasonably comprehensive guide on the mechanised syntax of UTP, including hints on how to convert from mathematical UTP and the keystrokes requires in Isabelle.
• Theory document. Essentially a developers manual for the core UTP Isabelle theories.
• Optics library. This AFP document explains the formalisation of state-spaces in Isabelle/UTP.