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