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.

See also the full paper and the slides.