[isabelle-dev] Isabelle/jEdit: by vs. .. on faulty proofs
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