[isabelle-dev] Redundant equations in function declarations

Tobias Nipkow nipkow at in.tum.de
Tue May 29 17:01:00 CEST 2012


Am 29/05/2012 16:32, schrieb Makarius:
> 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.

Rudeness is kindness: If the user writes something that is misleading and shows
that he has failed to grasp some problem, it is kinder to force him to see the
errors of his ways.

Tobias



More information about the isabelle-dev mailing list