Re: [isabelle] How to build a heap image

On Tue, 14 Jan 2014, Christian Maeder wrote:

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.

It depends what you a trying to do with COMP, which became out of use many years ago. A more current approach is to use the Pure "prop" marker (a special constant) to indicate the intended rule structure, and then use regular OF or THEN. This is for tools that do some low-level tinkering of rule; normal end-user applications use high-level infrastructure like locales and interpretation.

To ease the initial transition to the current Isabelle2013-2 release, here is a definition of the old attribute for your own theory context:

attribute_setup COMP = {*
  Attrib.thm >> (fn B => Thm.rule_attribute (fn _ => fn A => A COMP B))

The 'attribute_setup' command is described with some basic examples that can be combined with the above NEWS to produce that Isabelle/ML snipped.

What is still missing in the Prover IDE is some hyperlink from formal entities like 'attribute_setup' to the corresponding documentation. The manual has that markup already, but the connection in the user interface is not yet there.


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