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



Dear All,

I would like to provide a brief remark with regard to my last question on
the mailing list: "How to make Eisbach's match functionality available from
Isabelle/ML?". While I am still genuinely interested in finding an answer
to the question, it seems that it will no longer have a significant impact
on my work and, therefore, finding an answer has a very low priority for
me. Generally, you can view this email as a retraction of the question.

Kind Regards,
Mikhail Chekhov

On Sun, Oct 4, 2020 at 8:47 PM Mikhail Chekhov <mikhail.chekhov.w at gmail.com>
wrote:

> 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.