# Re: [isabelle] subst question

On Wed, 12 Oct 2005, Jeremy Dawson wrote:
> 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?
> 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")]) ;
Just note that using standard within a proof is a very bad idea -- its
purpose is to conclude a sequence of reasoning, producing a certain normal
form with some internal rearrangements. Even worse, standard only works
properly in a top-level theory context, but messes up the proof state in
the presence of local assumptions, locales etc.
Functions like prove_goal, prove_goalw_cterm are of the same category, and
are better avoided.
> see the reference manual s3.5.1 and s3.1.4
The reference manual is slightly outdated, and will be replaced
eventually.
Makarius

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