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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
