[isabelle] Creating new Isar theorem attributes



Hi,

I would like to use the isabelle commands addE2, addD2, addSE2, and addSD2 (see Provers/classical.ML) to extend the current claset in Isar. I am hoping these commands will cut down on the search space that "auto" has to explore. 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.

Thanks,
-john






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