*To*: Søren Haagerup <shaagerup at gmail.com>*Subject*: Re: [isabelle] Problem with frule_tac substitution*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 8 Feb 2011 08:14:09 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTintffdFWbPvwpnHi1gtPs8tr2PnwTKaCDW9TsJB@mail.gmail.com>*References*: <AANLkTintffdFWbPvwpnHi1gtPs8tr2PnwTKaCDW9TsJB@mail.gmail.com>

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.

**References**:**[isabelle] Problem with frule_tac substitution***From:*Søren Haagerup

- Previous by Date: Re: [isabelle] Quantifying over conditions
- Next by Date: Re: [isabelle] Problem with frule_tac substitution
- Previous by Thread: [isabelle] Problem with frule_tac substitution
- Next by Thread: Re: [isabelle] Problem with frule_tac substitution
- Cl-isabelle-users February 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list