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

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

Previous message (by thread): [isabelle-dev] Global build failures of the AFP in the testboard
Next message (by thread): [isabelle-dev] Software and Pyramids
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

Hi,

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

Previous message (by thread): [isabelle-dev] Global build failures of the AFP in the testboard
Next message (by thread): [isabelle-dev] Software and Pyramids
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the isabelle-dev mailing list