[isabelle] Method setup with arguments


Suppose I have already defined a ML function my_tac that takes a term as
input and returns a tactic, now I want to setup a method (here called
method1) to wrap it up. Is there a way to pass a term as an argument of the

For example, suppose I want to use method1 inside an Eisbach method called

method method2 = (match premises in P:"?A /\ ?B" => <method1 P>)

How should I define the setup and parser for method1 so that I can pass the
argument P as a term to my_tac?

Thank you very much!


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