Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.
Am 22.04.14 14:15, schrieb Makarius:
Because they're insufficiently highlighted and not tracked through later
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and