Re: [isabelle] Creating new Isar theorem attributes



Thanks, Makarius. Unfortunately, the code I wrote isn't being executed by Isar. I've attached two files that illustrate the problem. The isar.thy file installs the new theorem attribute, and isar_test.thy tries to use it. I've instrumented the theorem attributes with "print" instructions, but none of them seem to fire.

Also, what is the difference between "local" and "global" theorem attributes? That is, when should I use Classical.put_local_claset versus Classical.put_global_claset?

Thanks in advance,
-john

Attachment: isar.thy
Description: Binary data

Attachment: isar_test.thy
Description: Binary data


On Nov 22, 2005, at 5:17 AM, Makarius wrote:

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.


	Makarius



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