[isabelle-dev] Redundant equations in function declarations
makarius at sketis.net
Thu Jun 28 22:25:36 CEST 2012
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.
More information about the isabelle-dev