Email Gateway (Aug 22 2022 at 12:48): Email Gateway (Aug 22 2022 at 12:48):From: Makarius <makarius@sketis.net>
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 http://sketis.net/wp-content/uploads/2016/02/Isar_in_2016.pdf
provide an overview for Isabelle users who know classic Isabelle/Isar
already.
(See also http://sketis.net/2016/the-isar-proof-language-in-2016)
Makarius
Email Gateway (Aug 22 2022 at 12:48):From: "Elsa L. Gunter" <egunter@illinois.edu>
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.
---Elsa
Email Gateway (Aug 22 2022 at 12:48):From: Makarius <makarius@sketis.net>
The Slides are a a slightly extended variant of the information in the
NEWS for Isabelle2016, with a bit more context.
The individual commands that are mentioned there are described in the
isar-ref manual as usual. (A few details might still require updating in
the time that is left before final lift-off).
Makarius
Last updated: Apr 24 2024 at 16:18 UTC