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

Makarius makarius at sketis.net
Tue May 21 14:20:06 CEST 2013

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.


More information about the isabelle-dev mailing list