*To*: Reto Kramer <kramer at acm.org>*Subject*: Re: [isabelle] subst question*From*: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>*Date*: Wed, 12 Oct 2005 08:43:08 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <DF61E1D8-6295-436B-9E45-AE30565F7344@acm.org>*Organization*: Australian National University*References*: <DF61E1D8-6295-436B-9E45-AE30565F7344@acm.org>*User-agent*: Mozilla Thunderbird 0.9 (X11/20041124)

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?Thanks, - Reto

> by (instantiate_tac [("y31", "fst")]) ; Actually I've found you get a less flaky proof by the following

by (PRIMITIVE standard) ; by (instantiate_tac [("y", "fst")]) ; see the reference manual s3.5.1 and s3.1.4 Jeremy

**Follow-Ups**:**Re: [isabelle] subst question***From:*Makarius

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

- Previous by Date: [isabelle] FMCO 2005: second call for participation
- Next by Date: Re: [isabelle] subst question
- Previous by Thread: Re: [isabelle] subst question
- Next by Thread: Re: [isabelle] subst question
- 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