Re: [isabelle] tactic in Eisbach method



Currently there is no standard way to directly access the run-time context inside of an Eisbach method. In general the use of the "tactic" method in Eisbach is not well supported, mostly
due to not handling ML antiquotations as one might expect. The usual approach here is indeed to first lift your underlying tactic into a method with method_setup.


> On 28 Sep 2015, at 8:24 pm, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
>
> Dear Eisbach experts,
>
> I would like to use the tactic method inside a method definition with Eisbach.
> Here is a minimal example:
>
>  method foo = (tactic {* Transfer.transfer_step_tac @{context} 1 *})
>
> Obviously, this does not work, because the proof tactic requires a context and using @{context} gives the compile-time context, while I should rather use the context at the invocation site. Is there a way to access the dynamic context from within an Eisbach method definition? Or do I have to wrap the tactic expression in a method definition first?
>
> Best,
> Andreas
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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