The forthcoming release of Isabelle2016 provides substantial refinements of the Isar proof language, after many years. This is a consequence of clarification of Isar internals, in order to support the Eisbach proof method language (by Dan Matichuk et al).

These Slides provide an overview for Isabelle users who know classic Isabelle/Isar already.