Re: [isabelle] How to build a heap image
Am 13.01.2014 21:11, schrieb Makarius:
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.
Right, I saw that entry, but still was not able to adjust our old proof.
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