Re: [isabelle] Creating new Isar theorem attributes

On Mon, 21 Nov 2005, John Matthews wrote:

> I would like to use the isabelle commands addE2, addD2, addSE2, and
> addSD2 (see Provers/classical.ML) to extend the current claset in Isar.
> Are there existing Isar theorem attributes for these commands? If not,
> how can I add them? I looked at context_rules.ML and attrib.ML, but
> didn't get much inspiration.

The relevant code is all in classical.ML, e.g. search for dest_local to
see how it is being done.

IIRC, addE2, addD2 etc. were introduced as an experimental feature during
early HOL-Bali development.  Now it appears to have been discontinued,
with only a few spurious occurrences are left in the sources.

Note that the "2" versions are quite dissimilar to the plain
dest/elim/intro attributes, as they are based on the internal wrapper
concept.  This is only available for fast/auto etc., but not blast; it
also makes it difficult to remove rules later on.


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