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



On Tue, 22 Apr 2014, bnord wrote:


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.

OK.  That is subsumed by:

 What is missing in the PIDE model is a global checkpoint to summarise the
 degree of "finishedness" of the overall project


	Makarius




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