[isabelle-dev] Redundant equations in function declarations

[Tobias Nipkow]

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