Re: [isabelle] How to build a heap image

On Mon, 13 Jan 2014, Christian Maeder wrote:

I see the old "COMP" attribute on that tracker item. The NEWS file for Isabelle2013 (February 2013) has the following entry on it:

* Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,
use regular rule composition via "OF" / "THEN", or explicit proof
structure instead.  Note that Isabelle/ML provides a variety of
operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
with some care where this is really required.

In current Isabelle2013-2 (December 2013) the Documentation panel provides quick access to this important file, which documents user-relevant changes. Morever, the Sidekick plugin provides some basic tree view for it, to get an overview of the long history of NEWS.


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