*To*: Reto Kramer <kramer at acm.org>*Subject*: Re: [isabelle] subst question*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 11 Oct 2005 09:10:55 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <DF61E1D8-6295-436B-9E45-AE30565F7344@acm.org>*References*: <DF61E1D8-6295-436B-9E45-AE30565F7344@acm.org>*Sender*: "L. Paulson" <lp15 at hermes.cam.ac.uk>

(rule blah) by (rule_tac y=fst in blah) somewhere. To solve the goal you gave, try apply (rule fst_conv [symmetric]) Larry Paulson On 10 Oct 2005, at 22:47, Reto Kramer wrote:

I find myself with the following subgoal: !! a b. a = ?y31 (a,b)How do I tell Isabelle to replace ?y31 with "fst" so that simp willsolve the goal?

**Follow-Ups**:**[isabelle] TLA thoery in src directory***From:*yongjian Li

**References**:**[isabelle] subst question***From:*Reto Kramer

- Previous by Date: [isabelle] subst question
- Next by Date: [isabelle] (no subject)
- Previous by Thread: [isabelle] subst question
- Next by Thread: [isabelle] TLA thoery in src directory
- Cl-isabelle-users October 2005 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