Re: [isabelle] How to make Eisbach's match functionality available from Isabelle/ML?
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] How to make Eisbach's match functionality available from Isabelle/ML?
- From: Mikhail Chekhov <mikhail.chekhov.w at gmail.com>
- Date: Tue, 6 Oct 2020 01:42:08 +0300
- In-reply-to: <CACDt=MJtubBeKSgrYgYH7t+WOTDCwALVrXntSHvySSm=4W-uxA@mail.gmail.com>
- References: <CACDt=MJtubBeKSgrYgYH7t+WOTDCwALVrXntSHvySSm=4W-uxA@mail.gmail.com>
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.
On Sun, Oct 4, 2020 at 8:47 PM Mikhail Chekhov <mikhail.chekhov.w at gmail.com>
> 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