[isabelle-dev] Redundant equations in function declarations

[Lawrence Paulson]

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.

Larry

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.