At the Isabelle Workshop 2016 in Nancy, I presented Isabelle/PIDE as IDE for ML. See also the outline of the main concepts and examples, together with the full demo setup.
Monthly Archives: August 2016
The Isar proof language in 2016
At the Isabelle Workshop 2016 in Nancy, I presented a paper about recent renovations of the Isar proof language:
This is a description of the Isar proof language as it stands today in 2016. This means the official release Isabelle2016 (February 2016), and the next release that is presumably published towards the end of the year. Relevant NEWS entries and updated portions from the Isabelle/Isar Reference Manual are summarized in one comprehensive article.