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