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?

Thanks,
- Reto




> by (instantiate_tac [("y31", "fst")]) ;

Actually I've found you get a less flaky proof by the following
which removes the 31 (which is particularly likely to vary after minor changes in your preceding proof steps)

by (PRIMITIVE standard) ;
by (instantiate_tac [("y", "fst")]) ;

see the reference manual s3.5.1 and s3.1.4

Jeremy








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