[isabelle] tactic in Eisbach method



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




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