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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and