[isabelle] How to make Eisbach's match functionality available from Isabelle/ML?



Dear All,

I would like to understand if there is a simple methodology that would
enable one to transform Eisbach's method match into a tactic that can be
used as part of another tactic in Isabelle/ML? It does not seem that the
public interface of MATCH_METHOD allows for this at the moment. However, it
is interesting to note that the signature of MATCH_METHOD contains the
following comment: "FIXME proper ML interface for the main thing".

What would be the easiest workaround for this problem? On the other hand,
if a solution does not exist (apart from copy-pasting parts of the
implementation), would it be too much to ask to convert my query into a
feature request?

Kind Regards,
Mikhail Chekhov



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