[isabelle-dev] Isabelle/jEdit: by vs. .. on faulty proofs

[Makarius]

On Thu, 25 Apr 2013, Lars Noschinski wrote:

> I just noticed (Isabelle rev. 30624dab6054) that "by" allows finishes a proof 
> (even if the proof is faulty), while ".." only finishes a proof if it can 
> actually prove the goal.
>
> Is this intended behaviour or just an oversight?

It is a consequence of 'by' being forked and '..' not.  This affects the 
way errors are propagated.

I would like to refine error reporting and recovery from errors at some 
point, such that the nesting structure of proofs are fully observed, 
independently of the accidental forks.


 	Makarius