Re: [isabelle] subst question



Makarius wrote:
On Wed, 12 Oct 2005, Jeremy Dawson wrote:


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.

 > 	Makarius


Alternatively to using standard, do

by (PRIMITIVE zero_var_indexes) ;

This has less effect on the remainder of the proof state,
in particular it doesn't turn hypotheses of the proof state
into premises

Jeremy






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