Re: [isabelle] subst question



It's easier to avoid this sort of problem at an earlier stage in the proof, e.g. replacing

    (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 will solve the goal?







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