Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.



On Tue, 22 Apr 2014, bnord wrote:

I'm also very much against the "insert a sorry" approach. I'd embrace an "oops" version discarding the last goal.

Why this? Proofs are conceptually irrelevant in various respects. Local skips are done in many situations already, with increasing tendency in the past 7 years.

What is missing in the PIDE model is a global checkpoint to summarise the
degree of "finishedness" of the overall project, or rather an overview of the inevitably unfinished parts. Right now, users have to do this via eye-balling on the Theories dockable.


	Makarius




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