[isabelle] Method setup with arguments



Hi,

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
method?

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

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!

Zhe 




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