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.
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