[isabelle-dev] Redundant equations in function declarations

[Makarius]

On Mon, 4 Jun 2012, Lawrence Paulson wrote:

> I don't think underlining would make much difference, because people are 
> already used to ignoring underlined material in Microsoft Word.

They don't ignore it in Eclipse when programming in Java -- the compiler 
won't let them in the end.  In contrast, MS Word will allow to ship a 
document with spelling errors.

Anyway, I've left the old TTY/PG model behind long ago, and now we need to 
move forward to more and more refined feedback on the status of the text, 
mainly based on the principle of annotating the source (via squiggles 
etc.), but also by some kind of overview or digest of the degree of 
particiality of formal checking so far.


 	Makarius