Re: [isabelle] Telling auto to use an eisbach method
I don't know the details of what you are trying to do. Maybe it could be
tackled by a simproc (which basically also says, do something special on
goals of a specific shape)?
On 09/01/2016 11:17 PM, Joachim Breitner wrote:
> Dear list,
> Iâm current in the process of following a Coq course using Isabelle
> (more as a FingerÃbung), and there I see some nice use of tactics, such
> - If you find a goal of this shape,
> - invoke that particular rule
> - with an instantiation calculated from the current goal state.
> In this case, the instantiation includes a set of names to avoid. I
> have posed my question about that part at
> (and now there is an Eisbach tag), but I am also wondering:
> How do I best integrate this into an (otherwise) nicely automated proof
> using our beloved auto?
> Conceptually, to me, the custom method is just a smart version of an
> introduction rule. But clearly I cannot just give a method as an
> argument to autoâs "intro:".
> Is there any other way to tell auto: âWhen you try introduction rules,
> well, also try running this given method?â
> If not, should there be such a way?
This archive was generated by a fusion of
Pipermail (Mailman edition) and