Re: [isabelle] Problem with frule_tac substitution



It is ?b2.2 in the new subgoal, but ?b2.0 in the original theorem.

Generally, avoid explicit instantiations if you can.

Larry Paulson


On 7 Feb 2011, at 14:48, Søren Haagerup wrote:

> Isabelle says "No such variable in theorem: ?b2".
> Trying with
> apply(frule_tac h="h" and f="f" and c="catafunc f b1" in promotion_theorem)
> instead, I see that b2 shows up as ?b2.2.






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