Re: [isabelle] The Isar Proof Language in 2016
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).
an overview for Isabelle users who know classic Isabelle/Isar already.
(See also http://sketis.net/2016/the-isar-proof-language-in-2016)
This archive was generated by a fusion of
Pipermail (Mailman edition) and