Re: [isabelle] term abbreviations?



On Thu, 20 Mar 2008, David Streader wrote:

> In constructing some proof  that have complexe goals formaed by unfolding
> locale definitions
> I have been  cut and pasting  the goal  in to a show statment
> 
> show "......complex gaol ...." (is  patten)
> 
> After which I only refer to the patten. Is there a term abbreviation for 
> current gaol or other method to avoid the cut and pasting? david

Maybe you just need the ?thesis abbreviation, which always refers to the 
conclusion of the last goal statement in the text (not the proof state!).


	Makarius






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