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



On 10/24/2010 08:19 AM, Alexander Krauss wrote:
Hi Sylvia,

2. Manually lift some_theorem into your "goal context" using Thm.lift_rule. Then, the schematic variables become parameterized over the goal parameters (i.e. they are now of function type). You can then instantiate them as you need. To apply the rule, you would then use
some variant of compose_tac.

Sylvia,

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

Jeremy






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