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