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




Am 22.04.14 14:15, schrieb Makarius:
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?
Because they're insufficiently highlighted and not tracked through later proofs.
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.