Re: [isabelle] The Isar Proof Language in 2016

Dear Makarius,
Where can I find the documentation giving the full formal syntax and semantics of Isar in 2016, particularly that of the 2016 Isar Proof language? I could not find it at the link you provided below, but I do confess I did not try every link in the side column.

On 2/4/16 8:25 AM, Makarius wrote:
Dear Isabelle users,

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.

(See also


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.