[isabelle] The Isar Proof Language in 2016



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




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