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.

Thanks Christian

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.