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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
