[isabelle-dev] Redundant equations in function declarations

Lawrence Paulson lp15 at cam.ac.uk
Tue May 29 16:48:57 CEST 2012

I'm not talking about user interfaces or models. I am saying that function definitions containing entirely redundant equations should be rejected, also in batch mode.


On 29 May 2012, at 15:32, Makarius wrote:

> The warnings were shown nicely in the Prover IDE, although some fine points still need to be addressed.  It is better to invest the time here, than to optimize for the old Proof General model, which tends to require more rudeness for messages to be seen by the user.

More information about the isabelle-dev mailing list