Re: [isabelle] subst question



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?

I looked up theorems containing "fst", this included in the list:
Product_Type.fst_conv: fst (?a, ?b) = ?a

This suggests the following applucation of rule:

apply (rule Product_Type.fst_conv[symmetric])


best,
lucas





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