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

Lars Noschinski noschinl at in.tum.de
Thu Apr 25 12:18:49 CEST 2013


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?

   -- Lars

More information about the isabelle-dev mailing list