Re: [isabelle] Writing a specific rule_tac application on ML level



Look at term_lift_inst_rule in tactic.ML, I've previously used it for (I think) something like what you're trying to do

that function no longer exists:

http://isabelle.in.tum.de/repos/isabelle/rev/07a8904f8fcd

Alex





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